Subject: Re: expressiveness and reuse
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Tue Feb 05 2002 - 06:49:03 PST
EISNER@il.ibm.com wrote:
> anthony,
>
> >So my request is for IBM and Motorola to indicate how they will (or do)
> fulfil
> >requirement R45(a): the language must support the definition of
> >named assertions.
> >I suggest that there should be names of instances of properties, and that
> >the names should be useful from outside the language, not (or not
> >just) accessed within it - which means that it should be clear to a reader
> >just what the property attached to the name is saying.
>
> can you clarify what you mean by names of instances of properties, as
> opposed to named properties? i.e., if it is possible to name a property,
> say "anthony", and then say
>
> assert anthony;
> assume anthony;
You could define a generic property, say "obliging":
obliging(r,w,g) = forall x: AG((r & (w = x)) -> AX(g & (d = x))),
and then instantiate it as
obliging(request_to_cindy, wish, grant, done)
The instance of the property could have the name "cindy_is_obliging".
I want to be sure that one can identify instances of properties clearly.
Note: I'm not specifically requesting this way of defining generic properties
-
just that, if there are ways of defining generic properties, then instances of
these properties can be clearly identified, not just the generic properties.
>
>
> does that do what you are looking for, or do you mean the ability to give
> an instance name to a property, just as you give an instance name to an
> instance of a module? if you mean the ability to give an instance name,
> how would such an instance name be used? also, what does it mean that the
> names should be useful "from outside the language"? examples would greatly
> aid my understanding.
>
As for being useful "from outside the language":
First, how the name would be used in the language - this might be if one had
language constructs such as "assume" and "assert":
assert cindy_is_obliging;
Outside the language, the names could be used in a simple language for
operating a tool that refers to the specification: e.g.
ignore cindy_is_obliging
where "ignore" is not a construct of the standard language.
Or perhaps
prove P1 assuming each selection of 3 from (A1,A2,A3,A4,A5)
I should perhaps say that I found it easier to envisage how properties would
be
clearly identified in Sugar than in CBV, where the properties appear to be
slipped in to a story.
Anthony
>
> thanks,
>
> cindy.
>
> Cindy Eisner
> Formal Methods Group Tel: +972-4-8296-266
> IBM Haifa Research Laboratory Fax: +972-4-8296-114
> Haifa 31905, Israel e-mail:
> eisner@il.ibm.com
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Tue Feb 05 2002 - 06:50:39 PST