Re: annotation for implies

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

[comments from Peter and then Andrzej]

> According to Peter Mosses:
> 
> >> It seems that the only difference between regarding the (hopefully)
> >> implied axioms as part of the spec or not is in the case that they are
> >> not actually consequences of the other axioms.  I don't know much
> >> about methodological issues, but I guess that anyone reading a spec
> >> will probably take the implied axioms on trust, regardless of their
> >> syntactic status, so I'm inclined to agree with you (Bernd) that one
> >> might just as well regard them as part of the spec.  Presumably all
> >> the annotated axioms should follow from all the non-annotated ones -
> >> maybe inductively, if the spec is a free extension (?).
> 
> I thought the basic rule was that annotations have no impact on the
> semantics. Hence we have two choices:
> 
> (a) Revising CASL V1.0 to extend it with a further class of axioms (implied
> axioms) with a corresponding revision of the semantics (a spec with implied
> axioms that are not actually consequences of the other axioms will be
> ill-formed or inconsistent).

(a) is not an option for CASL v1.0, only for some later version, I guess.

> (b) Keeping what we have at the moment and considering implied axioms as
> pure annotations, with no effect on the semantics, and expecting that some
> tool will be able to derive the corresponding proof obligations and submit
> them to some theorem prover.

(b) is in line with Markus's original proposal.  I agree that
ANNOTATIONS should have no impact on semantics.  But I still think
that you are missing a further option (my understanding of Bernd's
proposal): 

(c) Axioms that have the %implied annotation should contribute to the
semantics as if the annotation wasn't there.

> BTW, of course implies should not be treated too syntactically. An implied
> axiom is an axiom that holds for the class of models of the considered spec
> (hence various proof rules may have to be used, including of course
> induction when free or generated is around).
> 
> >> My personal preference would be to annotate each axiom with %implied
> >> at the start.  I'm afraid that it would be too confusing to start
> >> reusing keywords to form annotations.
> 
> This sounds good to me too.
> 
> >> If we're to incorporate any such annotation in the new release of the
> >> Summary, it had better be proposed on cofi-language rather soon, I think.
> 
> Perhaps we should take more time to think the issue more deeply.

I too am uneasy about making decisions about annotations without a
wider discussion.  But it appears that we are all rather busy, and
perhaps it is better to adopt some proposal now: it can probably be
changed later without much trouble, since annotations are supposed to
be flexible and need not be recognized at all by tools.

Cheers,

-- Peter
_________________________________________________________

and now Andrzejs comments:
==========================

In a spare minute (literally, no more can be expected from me these
days, sorry!), a brief reaction to the recent letter from Peter on
annotations for "implied axioms", with a huge apology from me if I am
misinterpreting what I read, which is quite likely, since I have
avoided any involvement in the discussion on annotations at all.

Two point nevertheless:

> > The \annoimpl annotation does not change the
> > semantics of a specification,

Of course it does not: no anotation changes the semantics of CASL
specifications, as defined in the CASL semantics document.
Annotations are and should be disregarded there!

Then, i can see a reason for letting "implied axioms" be outside the
spec. If the implied axioms are within a group spec then I would
require that they follow from the other axioms in the group (a formal
statement might be that the classes of models of the group with and
without the implied axioms coincide). There would be no natural place
then to state "implied axioms" that "follow from all the non-annotated
ones (...) inductively, if the spec is a free extension". As I see it,
this would imply a very context-dependent reading of axiom groups
(including "implied axioms"), which I do not like. On the other hand,
for freely constrained specifications, the axioms that are implied by
such specs, written out of the spec, would be allowed to follow
"inductively" in the most natural fashion: they simply have to hold in
all (free, in this case) models of the spec.

And: I like the syntax

  SPEC %implies GROUP-SPEC

Peter proposes, perhaps even a generalisation to 

  SPEC %implies SPEC

might be considered to be used to state refinement between
specifications as an anotation.

Very best,

Andrzej