Final Proposal for Annotation IMPLIES

[Markus Roggenbach <roba@informatik.uni-bremen.de>]

[please note the deadline of October 24th for reactions on this proposal]

Final Proposal on an Annotation IMPLIES
=======================================

by Markus Roggenbach, Michel Bidoit, Bernd Krieg-Brückner, and Till
Mossakwoski

Contents:
=========
  I. Proposal
 II. Discussion of the Proposal
III. A Short History of %implies


I.Proposal:
===========

The annotation `%implies' may immediately follow either

-> a `then' keyword within an EXTENSION, in which case, let SP be the
part of the EXTENSION just up to, but excluding the annotated `then',
and let SP' be the specification immediately following the `then'; or

-> the equals sign within a SPEC-DEFN, in which case, let SP be the
union of the imports, extended by the union of the parameters, and let
SP' be the body of the specification definiton.

The annotation '%implies' is well-formed iff

C1) the signature of (SP then SP') is the signature of SP and
C2) SP' is a BASIC-SPEC.

A well-formed '%implies' annotation holds iff

C3) the model class of (SP then SP') is the model class of SP.


II. Discussion of the Proposal:
===============================

1) The proposal is formulated in analogy to the subsection C.5.2.4
"Semantic Annotations" in the language summary, page C-17.

2) This proposal differs from the presentation at the meeting in Bonas
in
the second condition C2):

 SP' is a BASIC-SPEC

In the presentation at Bonas we proposed that SP' shall be a nonempty
list of IMPLIES-ITEMs, where

IMPLIES-ITEM  ::= free type/types DATATYPE-DECL; ...; DATATYPE-DECL;/
          |  generated type/types DATATYPE-DECL; ...; DATATYPE-DECL;/
          |  var/vars VAR-DECL; ... VAR-DECL;/
          |  var/vars VAR-DECL; ... VAR-DECL
                           "." FORMULA "." ... "." FORMULA;/
          |  axiom/axioms FORMULA ; ...; FORMULA;/

Don suggested in Bonas to include sort generation in the
IMPLIES-ITEMs, i.e. to add the line
          |  generated { SIG-ITEMS ... SIG-ITEMS } ;/
to this grammar.

Including this line means that an IMPLIES-ITEM is a BASIC-ITEMS (see
page C-2 in the language summary) excluding only SIG-ITEMS. Thus we
propose to include SIG-ITEMS also. This allows additionally for
operation attributes after an %implies and does not provide problems
due to the first condition C1) on the signatures.

3) For the methodological motivation of %implies see the "Second
Bremen Proposal on an Annotation IMPLIES"

http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00015.html

and Michels comments to this proposal

http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00017.html



III. A Short History of %implies:
=================================

March 1999:
~~~~~~~~~~~
Michel suggests a semantic annotation implies at the meeting of the
Language Design Task Group in Amsterdam. Michel is asked to present a
proposal for this annotation.

http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00003.html

June 1999:
~~~~~~~~~~
In agreement with Michel (he writes: "I will be more than happy to
react on your proposal") there is a first Bremen proposal on implies
giving rise to a discussion on cofi-language@brics.dk.

http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00005.html

http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00006.html

July 1999:
~~~~~~~~~~
The "Second Bremen Proposal on an Annotation IMPLIES" tries to
summarize the discussion in a new proposal. Michel is willing to
support this proposal with some comments and restrictions.

http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00015.html

http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00017.html

September 1999:
~~~~~~~~~~~~~~~
The "Second Bremen Proposal on an Annotation IMPLIES" with the
modifications of Michel is presented at the meeting of the Language
Design Task Group in Bonas.

See the minutes of this meeting
http://www.brics.dk/Projects/CoFI/MailingLists/cofi-language/99/msg00020.html

--
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------