[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Second Bremen Proposal on an Annotation IMPLIES
Second Bremen Proposal on an Annotation IMPLIES
===============================================
by Markus Roggenbach, Till Mossakwoski, and Bernd Krieg-Br"uckner
The discussion in the cofi-language mailing list brought up several
questions concerning the annotation "%implies", which we try to
summarize here -- each combined with a short statement of us. The
arguments for our answers can be found in the appendix.
1) Why do we need an annotation "%implies"?
-------------------------------------------
It helps -- from a methodological point of view -- answering the
question: "Am I specifying the right thing?"
2) What "part" of a spec should be annotated with "%implies"?
-------------------------------------------------------------
Only axioms, combined with an appropriate mechanism to declare
variables.
3) Shall the annotated axioms be part of the specification?
-----------------------------------------------------------
Yes.
4) What is an appropriate syntax for the annotation?
----------------------------------------------------
In the appendix we propose a grammar for the syntax. For a glimpse we
give you just an example:
spec FiniteSet [Elem]=
...
then %implies
vars x:Elem; S,T: FinSet[Elem]
. S subseteq T <=> (forall x: Elem. x elemOf S <=> x elemOf T)
end
I.e. the annotation "%implies" may only be inserted after the keyword
"then", followed by an non-empty sequence consisting of global variable
declarations, local variable declarations and axioms.
5) How is "%implies" related with the other annotations?
-------------------------------------------------------
Our proposal for the annotation "%implies" follows the same
syntactical scheme as the already approved annotations "%def" and
"%conservatively" (which we propose instead of "%cons") using the
keyword "then" as structering element. There is a clear distinction
between the meanings of "%implies", "%def" and "%conservatively".
======================================================================
APPENDIX
1) Why an Annotation "%implies"?
================================
This annotation is expected to help answering the question: "Am I
specifying the right thing?" This can be done by dividing the axioms
of operations and predicates into two classes: "normal axioms", which
define the operations and predicates, and "implied axioms". The
implied axioms specify properties that should follow from the normal
axioms.
A nice "side effect" of the annotation is that it helps to structure
consistency proofs: given a set N of normal axioms, and a set I of
implied axioms, (i) implies (ii):
(i) N is consistent, and for all axioms A of I holds: N implies A.
(ii) (N cup I) is consistent
2) What "part" of a Spec Should Be Annotated With "%implies"?
=============================================================
There are already possibilities to relate whole specifications in
CASL, e.g. via a VIEW or by one of the annotations "%def" and
"%conservatively", resp. The question is, what is the new concept of
the annotation "%implies"?
Peter and Andrzej suggested to allow a whole specification after the
"%implies":
SP %implies SP'
Andrzej suggested to express refinement with this construct.
Here are our objections against this:
(1) The syntax of annotations requires that annotations start
with a percent sign. Thus, "%implies SP'" would be an annotation
on the specification SP. However, we think that refinements
should have a more prominent status, and not be attached to
something else. E.g. they sould have a status simliar to other LIB_ITEMs
like views. Moreover, refinements are an important methodological
concept that should not be mixed up with specifying intended
consequences. If we wanted to re-use existing CASL constructs
for refinement at all, views would be much more adequate:
Instead of
spec sp = SP %implies SP' end
just write
spec sp = SP end
view v: sp to SP'
(the semantics is the same).
(2) If the point is not refinement, but just specifying intended
consequences, then it is not clear why a signature extension
should be allowed within the extended consequences.
Normally, stating that a signature extension does no harm
is the point of a conservative extension. I.e. in this case,
instead of
SP %implies SP'
we should write
SP then %conservatively SP'
Again, the semantics is the nearly same, except that
SP' now becomes part of the specification (but this
has to be the case anyway, see 3) below).
Thus the interesting aspect of "%implies" is that it introduces a
concept weaker than the annotation "%conservatively" or the CASL
construct of a view, namely: just axioms are allowed.
(BTW: This was Michel's original intention in Amsterdam.)
3) Shall the annotated axioms be part of the specification?
===========================================================
Note that something like
SP
%implies
ax1
ax2
...
or (with Peter's suggested syntax):
SP
%implies
{ ax1
ax2
...
}
is problematic.
Since tools should be able to easily ignore annotations,
we should devise a rule that an annotation always ends with the end
of the line (otherwise, the would have to know the specific
syntax for each annotation, which contradicts the way annotations
are introduced in CASL). Making each line part of the annotation
(by prefixing it with "%" and possibly some continuation symbol)
seems not to be a realistic option as it reads badly and is very
cumbersome; such a thing should be reserved for annotation generated
by tools.
So there are two options:
(1) Make implies part of the CASL syntax
(2) Use %implies as an annotation for a structuring construct
of the CASL syntax
The first option would allow to have the implied axioms not as part
of the specification. However, there are objections (not from us)
against doing this.
The second option means that we have to attach %imples to an existing
CASL construct, and the best-suited construct is "then".
However, this means that the implied axioms become part of the
specification.
Now this does no harm, it even has the positive effect
that provers can use the implied axioms before they have
been proven to be consequences of the specification
(of course, a proof obligation related to the %implies has to be
generated).
4) What is an approriate syntax for the annotation?
===================================================
We propose the following grammar (note that this is not a new grammar,
but a restriction of the proper CASL grammar)
SPEC ::= ...
| SPEC then %implies AXIOM-ITEM+
AXIOM-ITEM ::= var/vars VAR-DECL; ... VAR-DECL;
| var/vars VAR-DECL; ... VAR-DECL
"." FORMULA "." ... "." FORMULA ;
| axiom/axioms FORMULA ; ...; FORMULA ;
Thus a tool capable to deal with the annotation "%implies" has the
opportunity to do an addidional syntax test concerning the correct use
of the annotation: A specification with the annotation "%implies" is
legal iff the annotation "%implies" is followed by a non-empty
sequence of AXIOM-ITEMs (see grammar above), where an AXIOM-ITEM is a
global variable declaration, a local variable declaration or an axiom.
5) How is "%implies" related with the other annotations?
========================================================
There are two important connections with the already approved
annotations "%def" and "%conservatively":
(i) all these annotations follow the same syntactical scheme, i.e.
SP
then %annotation
SP'
where the keyword "then" is used as structuring element that separates
the non-annotated part from the annotated part of a specification.
(ii) there is a clear distinction between the meanings of the
annotations:
a) "%implies" vs. "%def":
For both annotations holds: any model of SP can be uniquely extended
to a model of (SP then SP').
The distinction is that in case of "%implies" the unique extension
of the model has to be the empty extension.
b) "%def" vs."%conservatively":
For both annotations holds: any model of SP can be extended to a
model of (SP then SP')
The distinction is that in case of "%def" the extension
of the model has to be uniquely determined.
Please note that if SP' consists only of AXIOM-ITEMs (see the grammar
above), the meaning of the annotations "%implies", "%def" and
"%conservatively" is the same.
Thus, methodologically, the usage is as follows
(in increasing order of complexity and decreasing order of projected
number of occurrences):
a) %implies: to indicate that only implied axioms follow
b) %def: to define extensions such as e.g. function definitions
c) %conservatively: to define other conservative extensions
The last option is least needed and thus justifies (in our opinion)
a rather longer name to alert to its rather complicated semantics
(and proof obligations).
--
--------------------------------------------------------------------------
Markus Roggenbach Phone +49-421-218-4683
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen roba@informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen http://www.informatik.uni-bremen.de/~roba
--------------------------------------------------------------------------