Constantine:
We already have the beginnings of a DECLARE form for this purpose, and
we intend to populate the description of DEFTHM and DEFINVARIANT
shortly. In brief:
(DEFTHM name truth-judgement)
is a statement that the logical term expression "truth-judgement" is
supposed to evaluate to true. This term may include evaluations of
program expressions, and may make reference to state. DEFTHM introduces
a proof obligation that must be successfully discharged. Once
discharged, the truth-judgment can be used as a rewrite rule in
subsequent proofs.
(DEFINVARIANT name truth-judgement)
is a much stronger thing. It says that truth-judgement must be true at
all control points in the program *except* where it is explicitly
suspended by the SUSPEND form. The SUSPEND form is part of the
programming language, and takes the form:
(SUSPEND (inv-name ... inv-name)
e1 ... en)
SUSPEND is lexically scoped. The main advantage of invariants is that
they allow proofs to proceed over very small fragments of program
evolution. They allow us, for example, to say things like:
if 'x' is a think of type linked-list-element, then
either (a) x is unlinked or
(b) there exists exactly one list containing x
Finally, we are looking at proofs based on static control flow analysis
following the work we did with MOPS. For this sort of thing, it is
sometimes useful to be able to hand-label particular forms in the source
program. Not yet clear how we want to do that, but probably:
(LABEL label-name form)
Many of the examples you gave can be handled by this.
> 6. Annotations might give hints to type inference engine. BTW the
> current syntax for type annotations is a bit out of the line from the
> rest as it does not use (S-expressions).
The decision *not* to use s-expressions here was intentional. "Hints" to
the type inference engine aren't appropriate. It's either a type
declaration or it isn't. If it is, declare it.
shap
_______________________________________________
bitc-dev mailing list
[EMAIL PROTECTED]
http://www.coyotos.org/mailman/listinfo/bitc-dev
