I'll separate the features of the proof editor into basically three groups:
- The must-haves that define Version 1.0 which I plan to do as part of my Master's research;
- should-haves which are optional, but very useful things. From this set I'll draw problems to be treated in my PhD research; and
- the can-haves which are optional, but still interesting things. The proof editor will provide a framework in which to tackle those problems in, but they will probably too much for a single thesis. That means, other students and researcher can pick from here and do interesting work.
To be clear about the last two points: I don't say that no-one else may do research on the number 2 problems or everyone else should do research on the number 3 problems. It's just my guess what I'll be able to cover in my thesis and what not. The first point is very important, because I think that's the basis for all of the other work. We need some kind of editor running to do anything which I'd like to do in my research. Furthermore, the basic editor will also help a lot in learning Programming Theory in exploring different variants of it, in doing larger, more realistic case-studies and last not least attracting new students interested in the subject.
Must-haves for Prototype 1
- a way to enter propositions and to prove them using the rules and laws in Ric's book, especially the context rules which are implemented by window inference.
- symmetry, transitivity, reflexivity and perhaps distribution and other laws are built-in to the prover, which means that they can be performed directly without using a general rule and find the respective laws to apply.
- a place listing all the laws with a very basic ability to search them (pattern matching, search by name).
- a place listing all the theorems which have been proven so far. (Each instance of doing window inference will open an additional place that states all the local assumptions for that inference window.)
- the logic (symbols, axioms and laws) provided inside of the prover must at least include:
- booleans, bunches, functions and quantifiers to do calculations in predicate calculus. (Having all this, we'll also add sets with little effort).
- numbers, strings, lists, assignment, dependent composition, ok, recursion, var and frame to do programming, i.e. write specifications and refine them to programs. (Having all this, we'll also add characters and texts with little effort.)
- propositions are entered using the keyboard, with some convenient way of entering symbols which are not on the standard keyboard. It will be taken into account that the operators of the logic have to be typed very often, even more often than most of the letters. So probably fixed keys should be assigned to the most important symbols and simple key-combinations to all other symbols. (Online-help for the mapping well be provided.)
- type checking is needed to implement instantiation.
- rules can be applied after selecting sub-expressions with the mouse and then select the rule from a menu. (Shortcut-keys are also available and shown in the menu.)
- proofs are shown below their hypothesis (the proposition they're proving), where a green check mark behind the hypotheses indicates a complete proof; and a red cloud with the label "magic" on it indicates a gap (unfinished place in a proof).
Since the programming (especially recursive refinements) needs some handling at the meta-level, we might have a working version 0.5 which is able to do some basic logic proofs, but does not yet include programming.
This list seems much longer than the following two, but this is just because it is much more detailed, while the others invoke big areas with terse words. All of the sections will become more detailed as work progresses. More milestones will be added and completed milestones get the most detailed documentation.
- the relation between specifications and programs is managed (somehow), including recursive refinements: a program is a specification that only uses executable operators and specifications that have been refined (somewhere)
- programs can be run: the user enters values for the state variables and gets back values for the state variables
Additions of special interest to me
- ways to store and retrieve theorems easily when they are needed
- procedures, modules, abstract data types.
- ways to divide and share the name space, so that large programs can be conveniently handled. (Models for this are Eiffel, B and LARCH.) Do this for programs and theories.
- case studies:
- library of generic algorithms and data structures
- hardware verification
- a CPU scheduler, memory manager, persistent storage facility, network interface (Q: how are those four called when they come together?)
- Unified Algebra and case studies with advanced mathematics (i.e. more than the basic integer-algebra used in most of programming)
Additions in which others might be interested
- calling other provers and using their results in a proof, with a justification that contains just the other prover's name
- concurrency and interaction (some of it will already be needed for some of the case studies).
- programming language: loops, assertions, functional programming
- soundness proofs and other theoretical treatments