[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] Concrete syntax examples (verbose style) [400 lines]
Dear CoFI members,
Please find below some examples written in the "verbose" form of the
concrete syntax. The examples are mainly a translation of the ones in
our initial proposal, shrunk to "basic items" [by commenting-out the
structuring constructs --PDM]. The examples have not been checked by
tools, so they might contain bugs.
There are a few points that are not (yet ?) in the official proposal
sent by Peter, but that could be included without too much
burden. [These points are concerned merely with the notation for
freely-generated datatype declarations, and that for comments and
annotations. --PDM]
Finally, my very personal comments about the all syntax will appear
in a separate message.
[Comments from others are welcome too, of course! --PDM]
Frederic
----------------------------------------------------
[When I get time for it, I'll make an Examples document for browsing
individual specs on WWW. Until then, please take care not to cite
more than necessary of this longish message when following-up. --PDM]
%% A few definition taken from the STEAM-BOILER case study (M. Bidoit and ali.)
sorts
PumpNumber generated by Pump1 | Pump2 | Pump3 | Pump4;
%% PumpState = { Open | Closed }
%% Currently we are missing a concise :-)) notation for free constructs
%% Something like
PumpState freely generated by Open | Close ; %% NOT OFFICIAL
%% or
PumpState = { Open | Close } ; %% NOT OFFICIAL
%% My understanding is that this should pose no problem for the verbose
%% style, but a syntax for the concise version is still to be found.
%% Physical Units
PhysicalUnit generated by
Pump(PumpNumber)
| PumpController(PumpNumber)
| OutputOfSteam
| WaterLevel;
%% Operation Modes
Modes generated by
Initialization | Normal | Degraded | Rescue | EmergencyStop
sorts S_Message generated by
MODE(Modes)
| PROGRAM_READY
| VALVE
| OPEN_PUMP(PumpNumber)
| CLOSE_PUMP(PumpNumber)
| FAILURE_DETECTION(PhysicalUnit)
| REPAIRED_ACKNOWLEDGEMENT(PhysicalUnit)
%% generic spec SET [sorts Item] = %% We miss the singular form for "sorts"
sorts
Set[Item] generated by empty
| __+__(Set[Item], Item)
operators
__-__ : Set[Item]*Set[Item] -> Set[Item]; %% Set Difference
card : Set[Item] -> Nat; %% Cardinal
__dans__ : predicate(Item*Set[Item]); %% Membership
__inclus__ : predicate(Set[Item]*Set[Item]) ; %% Set Inclusion
asserts
%% In the following axioms, I use as few parentheses as possible, to see
%% if default precedence looks reasonable. In practice, we will probably add
%% parentheses for readability
S1 = S2 iff forall x:Item . x dans S1 iff x dans S2 ;
not x dans empty ;
x dans (S + y) iff x = y or x dans S;
x dans (S1 + S2) iff x dans S1 or x dans S2;
x dans (S1 - S2) iff x dans S1 and not x dans S2;
S1 inclus S2 iff forall x:Item . x dans S1 implies x dans S2;
card(empty) = 0;
x dans S implies card(S + x) = card(S);
not x dans S implies card(S + x) = card(S) + 1 ;
variables x,y:Item; S,S1,S2:Set[Item]
%% spec COLLECTION_OF_NAMED_OBJECTS = %% NOT OFFICIAL
%% enrich conservatively NAMED_OBJECTS and NATURAL_NUMBERS by %% NOT OFFICIAL
sorts Collection generated by the_empty_collection
| __plus__(Collection, Object);
operators
__less_the_object_named__ : Collection*Name -> Collection ;
the_size_of__ : Collection -> Nat ;
__is_empty : predicate(Collection) ;
asserts
C is_empty implies C less_the_object_named n = C;
n = the_name_of O implies
C plus O less_the_object_named n = C less_the_object_named n;
not n = the_name_of O implies
C plus O less_the_object_named n =
C less_the_object_named n plus O;
the_size_of the_empty_collection = 0;
%% Prefix ops have higher precedence than infix.
the_size_of (C plus O) = succ(the_size_of C);
the_empty_collection is_empty;
%% Postfix ops have higher precedence than infix.
not (C plus O) is_empty ;
variables n:Name; C:Collection; O:Object
end
%% This one deals mostly with struturing stuff, but show how operators
%% would appear in morphism ?? NOT OFFICIAL
spec COMPOUND_SYMBOLS_ARE_NICE =
enrich
%% In the two following lines, the delimiters around operators will
%% probably not be the double quotes
LIST_WITH_ORDER[NATURAL] where (Elem => Nat, __<__ => __leq__)
and LIST_WITH_ORDER[NATURAL] where (Elem => Nat, __<__ => __geq__)
by asserts order[__geq__](l) = reverse(order[__leq__](l))
variables l:List[Nat]
end
QUESTION: if we had to give explicitely the domain of the predicates, what
would be the syntax ?? Something like (__<__: predicate(Elem*Elem) => ...)
would not be very appealing.
%% two "datatype" with all generators included...
sorts Color generated by Blue | Red | Green ;
List[Elem] generated by nil | cons(hd: Elem, tl: List[Elem]) ;
%% Another datatype but the list of generators is not yet fixed.
%% The datatype definition provides a first list of generators.
Record >
%% a first generators with two selectors.
<__.__>(First: E1, __.second: E2)
| make_record(E1, E2) %% make_record has no associated selectors.
asserts
%% Actually, these two axioms come from the above definition
First(<v1.v2>) = v1;
<v1 . v2>.second = v2;
variables v1: E1; v2: E2;
I know that Peter has other proposals about the use of notations like
__.second
[...but nobody else does yet! So I might as well reveal it here:
to allow the general use of `x.f' for applying unary functions f to
argument terms x. When the function is a selector like
second:Record-?->E2, this gives the usual notation for selecting
fields of records, familiar from various programming languages. It
also avoids the need for tokens like `.second' that mix SIGNS and
WORDS. More formally, one needs only to add the alternative:
Abstract Concrete Input Display
APPLICATION T ::= T.FS T.FS
to the proposed grammar. But I'm not fully convinced of the need for
this in CASL, it might be left to an extension if too controversial.
--PDM]
%% Several forms of subsort definitions:
sorts Positive, Zero < Natural ;
Natural, Negative < Integer;
PositiveAlt, NegativeAlt, ZeroAlt < IntegerAlt ;
Zero generated by zero ;
Positive generated by succ(pred: Nat) ;
%% Datatype with two embeddings as constructors.
sorts Nat generated by sorts Zero | sorts Positive ;
%% Alternative
sorts Nat generated by sorts Zero, Positive ;
%% Subsort defined by a predicate.
sorts Odd = { n: Nat . odd(n) }
%% Another definition of LIST with anonymous operations
generic spec LIST [sorts Elem] =
sorts List[Elem] generated by
empty
%% Will the following declarations be valid?
| __ : Elem %% Lists made of just one element
| __ __ : Elem, List[Elem]; %% anonymous cons
%% We could imagine declaring the operators with (Peter's private suggestion)
__(ELem)
| (__ __)(Elem, List[Elem])
%% [and allowing the corresponding function declarations to be written
%% directly --PDM]
%% but the real problem is: do we accept terms like:
%% one element list: e
%% a with anonymous cons: e1 e2 e3
%% If the declarations were not allowed we would have operation
| single: Elem -> List;
| add: Elem*List -> List;
operators
__is_empty: predicate(List[Elem]);
asserts
empty is_empty;
not single(e) is_empty ;
not add(e, l) is_empty ;
add(e, empty) = single(e) ;
variables e:Elem; l:List[Elem]
end
%% generic spec LIST_WITH_ORDER [sorts Elem;
%% operators __<__ : predicate(Elem*Elem)
%% %% assert usual axioms for <
%% ] =
sorts List[Elem] generated by
nil
| cons(hd: Elem, tl: List[Elem]);
operators
insert: Elem*List[Elem] -> List[Elem];
order: List[Elem] -> List[Elem];
asserts
order(nil) = nil;
order(cons(x,l)) = insert(x,order(l));
insert(x,nil) = cons(x,nil);
x < y implies insert(x,cons(y,l)) = cons(x,cons(y,l));
not x < y implies insert(x,cons(y,l)) = cons(y,insert(x,l));
variables x,y:Elem; l:List[Elem]
end
sorts Odd' = { n: Nat . odd(n) } ;
asserts
%% Actually the axioms are bogus since "pred" and "succ" are not defined !
%% beware: and and or cannot be mixed freely.
t in Odd' iff t = succ(zero) or
( t > succ(succ(zero)) and pred(pred(t)) in Odd');
pred(t) defined if t in Positive;
variables t: Nat
%%spec STEAM_BOILER =
%% enrich conservatively VALUES by
operators
C, M1, M2, N1, N2, W, U1, U2, P : Value;
dt : Value ; %% Time duration between two cycles (5 sec.)
asserts
%% These constants must verify some obvious properties
0 < M1 ;
M1 < N1 ;
N1 < N2 ;
N2 < M2 ;
M2 < C ;
0 < W ;
0 < U1 ;
0 < U2 ;
0 < P ;
dt = 5
%% That one comes from the specification of thew UNIX File system
%% spec PATH =
sorts Path ;
operators
the_first_part_of__ : Path -?-> Path ;
the_last_name_of__ : Path -> Name;
asserts
the_first_part_of p defined iff not p is_a_name;
not p is_a_name implies
the_first_part_of (n/p) =!= n / the_first_part_of p;
p is_a_name implies the_first_part_of (n/p) = n;
the_last_name_of n = n;
the_last_name_of (n/p) = the_last_name_of p;
variables n:Name; p:Path
%%generic spec SET[ELEM] =
sorts Set[Elem];
operators
empty: Set[Elem];
add: Elem*Set[Elem] -> Set[Elem];
the_empty_set : Set[Elem] ;
is_empty : predicate(Set[Elem]);
first: Set[Elem] -?-> Elem ;
rest: Set[Elem] -?-> Set[Elem];
asserts
the_empty_set = empty ;
first(add(x, s)) = x;
rest(add(x, s)) = s;
is_empty(the_empty_set);
not is_empty(add(x, s));
first(s) defined if not is_empty(s);
rest(s) defined if not is_empty(s);
variables x: Elem; s: Set[Elem]
end
%% a third version of SET[ELEM] where axioms are interspersed among operations.
%% For Set membership and Set inclusions, we use syntactic forms with a Latex
%% meaning
%%generic spec SET[ELEM] =
sorts Set[Elem] generated by
{} %% NOT OFFICIAL
| {__}(Elem) %% NOT OFFICIAL
| __+__(Set[Elem], Set[Elem]) ; %!Latex:$\cup$%!
%% The above latex "annotation" has a concise form since the source of the
%% mapping is known.
operators
is_empty__: predicate(Set[Elem]);
choose: Set[Elem] -?-> Elem ;
asserts
%% usual axioms on Sets are omitted.
is_empty {};
is_empty { x } ;
%% Beware: prefix ops bind tightlier than infix.
is_empty (S + S') iff is_empty S and is_empty S';
variables S, S': Set[Elem];
operators
__<__, __le__ : predicate(Set[Elem]*Set[Elem]) ;
%% "in" being a keyword, it is not a good idea to have an operator __in__
%% since its use would look like a in b, with a different meaning...
%% __in__ : predicate(Elem*Set[Elem]);
__is_in__ : predicate(Elem*Set[Elem]);
%% The correspondence between concrete and display syntax can be
%% given outside of the declaration. We cannot infer the source from the
%% location of the annotation so a more general synatx would exist to
%% define arbotrary associations.
%%
%!ELatex:"__<__", "\subset"%!
%!ELatex:"__le__", "\subseteq$%!
%!ELatex:"__is_in__"."\in"%!
asserts
{} le S;
{ x } le S iff x is_in S;
S + S' le S'' iff S le S'' and S' le S'';
S < S' iff S le S' and not S = S';
variables x: Elem; S, S', S'': Set[Elem];
asserts
not x is_in {} ;
x is_in { y } iff x = y;
x is_in (S + S') iff x is_in S or x is_in S';
choose(S) defined iff not is_empty S ;
choose(S) defined implies choose(S) is_in S;
variables x: Elem; S, S': Set[Elem]
end
sorts Set[Elem] generated by
{} %% NOT OFFICIAL
| {__}(Elem) %% NOT OFFICIAL
| __+__(Set[Elem], Set[Elem]) ;
operators
is_empty__ : predicate(Set[Elem]);
__is_in__ : predicate(Elem*Set[Elem]); %% __in__ would be a bad idea
__leq__, __<__ : predicate(Set[Elem]*Set[Elem])
assert
is_empty {} ;
not is_empty { x } ;
is_empty (S + S') iff is_empty S and is_empty S';
%% The following, functional, notation is also allowed:
%%"is empty __"(S + S') <=> "is empty __"(S) /\ "is empty __"(S') ;
(is_empty__)(S + S') iff (is_empty__)(S) and (is_empty__)(S') ;
not x is_in {} ;
x is_in { y } iff x = y ;
x is_in (S + S') iff x is_in S or x is_in S';
{} leq S;
{ x } leq S' iff x is_in S';
(S + S') leq S'' iff S leq S'' and S' leq S'';
S < S' iff S leq S' and not S = S';
variables x: Elem; S, S', S'': Set[Elem]
end
Thanks to Peter for dectecting many typos in an earlier version and
suggesting alternatives. All remaining errors are mine !!
[Thanks to Frederic for doing all the hard work of transforming the
examples from the original proposal! --PDM]