Subject: Re: SDL-News: Type specialization
From: Rick Reed TSE (rickreed#tseng.co.uk)
Date: Fri Jun 17 2005 - 23:14:00 GMT
Become an SDL Forum Society member <http://www.sdl-forum.org/Society/members.htm>
The originator of this message is responsible for its content.
-----From Rick Reed TSE <rickreed#tseng.co.uk> to sdlnews -----
haroud at haroudm#gmail.com wrote on 15/06/05 17:51:
> Is the following SDL code legal and fully defined
>
> newtype T inherits BOOLEAN
> adding literals Z,X;
> endnewtype;
>
> Context:
> -------------------------------
> dcl t T :=false;
>
> start;
> .....
> decision t;
> (=Z):
> ......
> (=X):
> ......
> (true):
> ....
> (false):
>
> enddecision;
An interesting question.
In SDL-92
=========
The literal names true and false are inherited by T.
No operators are inherited if they are not mentioned. See the clause in
Z.100 "If neither ALL or inheritance list is specified, the inheritance
operators are the equal and not equal operators only".
[NOTE: The clause in Z.100 (03/03) "the keyword ALL is implied if omitted"
only applies if there are actual context parameters.]
When not inheriting from Boolean, the inherited operators "=" and "/=" would
be
"=": T, T -> <<PACKAGE Predefined>> Boolean;
"/=": T, T -> <<PACKAGE Predefined>> Boolean;
But in this case the identifier of the result is <<PACKAGE Predefined>>
Boolean, and also becomes transformed to T.
So from inheritance we have the operators
"=": T, T -> T;
"/=": T, T -> T;
If all the operators were to be inherited the definition should have had
OPERATORS ALL. If all except "=" and "/=" were wanted the definition should
have had OPERATORS ("not", "and", "or", "xor", "=>", NOEQUALITY). The syntax
does not allow ALL and NOEQUALITY to be combined [which I regard as a design
error in Z.100(03/93) - and I was the rapporteur for drafting this part].
There is no implied "=" or "/=" operator for T, because it has an
<inheritance rule>.
So consider
NEWTYPE T INHERITS Boolean
ENDNEWTYPE;
Is this well-defined by SDL-92?
Inheritance in SDL-92 is defined by a "modeL", so it should be possible to
transform this into equivalent SDL without the model. The result is:
NEWTYPE T
LITERALS true, false;
OPERATORS NOEQUALITY;
"=": T, T -> T;
"/=": T, T -> T;
T!: Boolean -> T; /* hidden type casting operator*/
AXIOMS
/* derived from IO(t1, ..., tn) == S!(BTO(v1, ..., vn)) */
/* 5.3.1.11 Model page 138 Z.100 (03/93) */
"="(true, false) == T!("="(true, false));
"="(false, true) == T!("="(false, true));
"="(true, true) == T!("="(true, true));
"="(false, false) == T!("="(false, false));
/* similarly for "/=" */
"/="(true, false) == T!("="(true, false));
"/="(false, true) == T!("="(false, true));
"/="(true, true) == T!("="(true, true));
"/="(false, false) == T!("="(false, false));
/* derived from 5.3.1.11 Model page 138 Z.100 (03/93) */
/* there is no literal renaming so from */
/* for all ilv in S literals( */
/* for all blv in BS literals( */
/* Spelling(ilv) /= Spelling(il1),.., Spelling(ilv) /= Spelling(iln), */
/* Spelling(ilv) == Spelling(blv) ==> ilv == S!(blv);)) */
true == T!(true); /* no renames, spelling "true" */
false == T!(false); /* no renames, spelling "false" */
/* and hence a canonical axiom set can be derived */
/* "="(true, false) == false; */
/* "="(false, true) == false; */
/* "="(true, true) == true; */
/* "="(false, false) == true; */
/* similarly for "/=" */
/* "/="(true, false) == true; */
/* "/="(false, true) == true; */
/* "/="(true, true) == false; */
/* "/="(false, false) == false; */
ENDNEWTYPE T;
While this is clearly a well-defined data type, expressions of the form,
(t = true) cannot be used in a context where a Boolean is required, because
the type of t is T.
In Z.100(03/93), however, a "decision transfers the interpretation to the
outgoing path whose range condition contains the value given by the
interpretation of the question". Exactly what "contains" means is not
further defined, except that it is clear that it refers to a set of values
and where a single value true or false is given the intended evaluation is
clear.
A range condition "defines a range check" and "a range check is" ... "used
to determine the interpretation of a decision". This implies the range check
is evaluated. A single value such as "true" in the example is equivalent to
"= true", and for the question "t" is equivalent to "t = true". Here there
is some ambiguity in Z.100: the range check is required to be "true" but it
is not explicitly stated this has to be a Boolean value (which in this case
it is not). However, if the decision answer is for an Integer and is of the
form (1, 3, 5), in this case the terms are required to be Boolean, so it
seems reasonable this also applies for a single term.
The conclusion is that in SDL-92 the type T without is well-defined, but
the decision answers are not valid.
The addition of the literals X and Z give a type that is equivalent to
NEWTYPE T
LITERALS true, false, X, Z;
OPERATORS NOEQUALITY;
"=": T, T -> T;
"/=": T, T -> T;
AXIOMS
"="(true, false) == false;
"="(false, true) == false;
"="(true, true) == true;
"="(false, false) == true;
"/="(true, false) == true;
"/="(false, true) == true;
"/="(true, true) == false;
"/="(false, false) == false;
ENDNEWTYPE T;
In this case there are an infinite number of values of the type because
values such as
X = X, X = X = X, X = X = X = X,
X /= X, X /= X = X
X = Z, Z = X
are not equivalent to any other value. So while T is "well-defined" it is
unlikely to be what was intended, moreover the range check for t = Z is
never "true", even if the variable t has the value Z!
The example illustrates a issue with SDL-92, such that it is unlikely that
(if SDL-92 is implemented as defined) simple inheritance of Boolean would be
useful. To get what is probably intended, NOEQUALITY should be put in the
inheritance list and the "=" and "/=" should be explicitly defined for the
type to give Boolean results.
SDL-2000
--------
The example is syntactically legal SDL-2000: the NEWTYPE ... ENDNEWTYPE
syntax is allowed as a legacy syntax (see Annex B of Z.100).
User defined data types in SDL-2000 do not rely on axioms, but are
constructed. The meaning of "equality" is more complex, because it can be
applied to references sorts (objects) and to two values of different sorts
if these are compatible. Inheritance is, however. The literals of the base
data type are inherited, and the new literals are added.
Every data type inherits from the ABSTRACT data type Any which has the
operator equal defined. In Any this operator has the signature
equal(THIS <<PACKAGE Predefined>> Any, THIS <<PACKAGE Predefined>> Any)
-> <<PACKAGE Predefined>> Boolean;
The <<PACKAGE Predefined>> attached to the names ANY and Boolean are only
needed if these names are not unique, and make the name into an identifier.
If the names are unique they can be omitted and the signature written as
equal(THIS Any, THIS Any) -> Boolean;
The use of the keyword THIS is defined below.
The use of "=" in an expression represents an Equality-expression and when
both operands are non-reference sorts (that is not a reference sort defined
by as an OBJECT type, or a pid sort) for the Equality-expression to be valid
both operands have to be of the same sort. If there are no OBJECT types,
this is unchanged from SDL-92 and the Equality-expression is the application
of the equal operator for the data type.
However, a major difference from SDL-92 arises because a distinction is made
in operator signatures between those sorts of data that are transformed when
the operator is inherited and those that are not. Only if the sort of data
is preceded by the keyword THIS, is it renamed. So the Boolean data type
inherits the signature of equal from the ABSTRACT data type Any as
equal(THIS Boolean, THIS Boolean) -> Boolean;
and the type T inherits the signature as
equal(THIS T, THIS T) -> Boolean;
which can be denoted in an expression by "=" such as in (t = true). As this
does not result in a T value, the explosion of values does not occur. The
meaning given to the equal operator is defined in D.2.3 of Z.100(08/2002)
and essentially states the values are the same if and only if they are
represented by the same literal name. That is for T
equal(true, true) == <<TYPE Boolean>> true;
equal(true, false) == <<TYPE Boolean>> false;
equal(true, X) == <<TYPE Boolean>> false;
equal(true, Z) == <<TYPE Boolean>> false;
equal(false, true) == <<TYPE Boolean>> false;
equal(false, false) == <<TYPE Boolean>> true;
equal(false, X) == <<TYPE Boolean>> false;
equal(false, Z) == <<TYPE Boolean>> false;
equal(X, true) == <<TYPE Boolean>> false;
equal(X, false) == <<TYPE Boolean>> false;
equal(X, X) == <<TYPE Boolean>> true;
equal(X, Z) == <<TYPE Boolean>> false;
equal(Z, true) == <<TYPE Boolean>> false;
equal(Z, false) == <<TYPE Boolean>> false;
equal(Z, X) == <<TYPE Boolean>> true;
equal(Z, Z) == <<TYPE Boolean>> false;
The decision and range condition are not changed in SDL-2000, but the range
check gives a Boolean result so the decision answers are valid.
The conclusion is that for SDL-2000 the example is well-defined and T has
exactly 4 values.
The answers (=Z) and (=X) could have been written (Z) and (X) with the same
meaning.
-- Rick Reed - rickreed#tseng.co.uk Tel:+44 15394 88462 Mob.:+44 7970 50 96 50--End text from Rick Reed TSE <rickreed#tseng.co.uk> to sdlnews --- For extra SDL Forum Society benefits join at <http://www.sdl-forum.org/Society/members.htm>
This archive was generated by hypermail 2a23 : Thu May 09 2013 - 16:05:50 GMT