[m-dev.] assertions summary
Fergus Henderson
fjh at cs.mu.OZ.AU
Fri Jul 23 06:34:46 AEST 1999
I'll use the term "statement" as a generic term to mean any statement
by the programmer which is supposed to convey some information about
the semantics of their program. This includes even ordinary clauses,
as well as other kinds of assertions/specifications/promises/whatever.
There are several different categories of statements.
Statements can be categorized based on the answers to the following questions:
* Do they _define_ the program's declarative semantics?
Or are they instead merely statements _about_ the (intended) semantics?
* When will they checked?
* Can the compiler/optimizer rely on them?
* Are they executable?
Here's some more detail about each question:
* Do they define the program's declarative semantics?
The operational semantics for Mercury programs is defined in terms
of the declarative semantics. So if a statement forms part of the
definition of the program's declarative semantics, it means that
the compiler/optimizer can rely on it.
* When will they checked?
The answer here may be
- at compile time (definitely)
e.g. `is semidet'
- at compile time (optionally)
e.g. `pragma check_termination(p/2)'
- at run time (optionally)
e.g. preconditions, postconditions
This is also what Lee called "at debug time";
it means at run time, when you have compiled with
appropriate run-time checking enabled.
- at run time (definitely)
Efficiency concerns will mean that most run-time
checks will be optional, but I suppose some might be
mandatory.
- unchecked (except perhaps by theorem provers...)
* Can the compiler/optimizer rely on them?
The answer to this question is in fact implied by the previous two.
The compiler is allowed to rely on statements only if
(a) they are part of the declarative semantics
OR (b) they have been checked
* Are they executable?
If the answer is yes, then they must be mode- and determinism-correct.
Based on these questions, I've devised a way of categorizing statements.
As usual, comments welcome; in particular, you might have some suggestions
about better names for some of these categories.
The two most broad categories are "contracts" and "definitions".
Contracts specify statements about what the program's semantics are
supposed to be. They must not be relied on by the compiler, unless
they have been checked. Definitions define what the program's declarative
semantics actually are. The compiler is allowed to rely on them.
Definitions can be divided into "clauses" and "promises".
Clauses must be executable, and hence have to be mode- and
determinism-correct, whereas promises need not be executable.
Clauses are defined using facts and rules, with completion semantics,
whereas promises can be arbitrary formulae.
Contracts can be divided into statically checked contracts,
runtime checked contracts, and unchecked contracts. Statically checked
contracts are checked at compile time. Runtime checked contracts
are checked at runtime, and must therefore be executable.
Unchecked contracts need not be checked at all, but can of course
optionally be checked using theorem provers.
The following table summarizes these categories.
-------------------------------------------------------------------------------
Category Part of the Are they Checked Can compiler
subcategory semantics? executable? rely on them?
----------- ----------- ----------- ----------- -----------
* definition yes _ _ _
* clause yes yes no yes
* promise yes no no yes
* contract no _ _ _
* statically checked no N/A compile time yes
* runtime checked no yes runtime no
* unchecked no no no no
-------------------------------------------------------------------------------
In addition to the above classification, statements can also be
divided depending on the form of the assertion they are making.
Treating particular forms of assertions specially is essential to
make static checking and runtime checking feasible.
Contracts which state whether or not particular formulae are even
meaningful are called "admissibility constraints". Contracts which
state whether particular formulae should be true or false are called
"success set constraints".
In what follows, "Formula" is any arbitrary formula,
"ExecutableFormula" is a mode- and determinism-correct formula,
and "TypeFormula" is a formula containing only type assertions
and in a simple enough form to be statically checkable (the details
depend on the type system).
Category Form of the assertion
-------- ---------------------
* definition
* clauses Atom <=> ExecutableFormula
* promise Formula
* `:- promise' declaration Formula
* transformation declaration Formula <=> Formula
(plus a hint that the RHS is more
efficient than the LHS)
* call to promise_only_solution(P) ( (P(Output1), P(Output2))
=> Output1 = Output2 )
* "mode-determinism assertions"
* is det/multi/cc_multi all [Inputs] some [Outputs]
P(Inputs, Outputs)
* contract
* statically checked
* admissibility constraints
* type definitions well_typed(Var:T) => TypeFormula
* pred/func type declarations admissible Atom => TypeFormula
* success set constraints Formula
* mode declarations Atom => well_typed(Inputs) =>
well_typed(Outputs)
* determinism declarations
* is det/semidet all [Inputs] (
(P(Inputs, Outputs1),
P(Inputs, Outputs2))
=>
Outputs1 = Outputs2)
)
* runtime checked
* admissibility constraints
* type invariants well_typed(Var:T) => ExecutableFormula
* pred/func admissibility decls admissible Atom => ExecutableFormula
* success set constraints
* complete specifications Atom <=> ExecutableFormula
* postconditions Atom => ExecutableFormula
* "failconditions" not Atom => ExecutableFormula
* unchecked
* admissibility constraints
* type invariants well_typed(Var:T) => Formula
* pred/func admissibility decls admissible Atom => Formula
* success set constraints Formula
* complete specifications Atom <=> Formula
* postconditions Atom => Formula
* "failconditions" not Atom => Formula
-------------------------------------------------------------------------------
Well, I guess that was all a bit complicated. There are a _lot_ of
different kinds of statements or assertions that we would like to make.
This raises the question: do we want or need different syntax for each
of them?
First, the distinction between definitions and contracts is important to the
user, and should definitely be reflected in the syntax, IMHO.
Second, I would argue that we do want different syntax for all the statically
checkable contracts, e.g. type, mode, and determinism declarations,
partly because it is important for the user and the compiler to be able to
easily distinguish such contracts, and partly because specialized syntax
can be much more consise for these kind of contracts.
(At any rate changing that would be pretty infeasible at this point,
so I don't think I will get much argument here).
The same principle applies to declarations about mutual exclusion etc.
for improved determinism analysis, as advocated by ROK et al.
That leaves the contracts which are not statically checkable.
For these, I think it is important for the user to know (and to be able to
control) which assertions will be checked at runtime and which will not.
So that too should be reflected in the syntax.
The admissibility constraints involve meta-predicates, and so for them
I think there should probably be special syntax -- see my previous mail
in reply to Mark Brown. Also, these should be part of the type definitions
and pred/func type declarations, since they affect the semantics of the mode
declarations -- see Lee's paper in the book "Types in Logic Programming"
for more information about this.
For program transformations (along the lines of what was recently discussed
on the Haskell mailing list), as Lee pointed out, the compiler needs to know
more than just that two formula are equivalent -- it needs to know which one
is more efficient. So we may need some special syntax for that too.
But for most of the other kinds of statements, I don't think there is any
compelling need to use special syntax, and so to minimize the language
complexity I think we should try to use a generic uniform syntax for these.
So for promises, run-time checked success set constraints, and unchecked
success set constraints, I propose that we use the following syntax:
:- promise Formula.
:- check Formula.
:- spec Formula.
`:- promise' would be an unchecked assertion that the compiler can rely on.
`:- check' would be a success set constraint (e.g. a postcondition or a
"failcondition") that gets checked at runtime if runtime checking is enabled.
`:- spec' declarations would not be used by the compiler, but could be used
by the declarative debugger or other tools.
For `:- check <Formula>', the syntax allowed would actually be a bit
more restrictive: the <Formula> would have to be one of the following forms,
Atom <=> ExecutableFormula
Atom => ExecutableFormula
not Atom => ExecutableFormula
the `:- check' declaration must be in the same module as the declaration for
`Atom', and the ExecutableFormula would have to be well-moded for all of
the modes of Atom.
For transformations we could use the syntax `:- promise Formula == Formula';
this would be equivalent to `:- promise Formula <=> Formula' but with the
additional information that the RHS is likely to be more efficient than
the LHS. (This is very loosely analogous with the use of `==' in type, mode,
and inst declarations.)
I'm still undecided about syntax for admissibility constraints.
Comments?
--
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3 | -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to: mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions: mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------
More information about the developers
mailing list