?prevdifflink? - Blame
I. Syntactical differences between ISO VDM-SL and IFAD VDM-SL
a) Semicolon (";") is only used as a separator between subsequent constructs
(between function definitions, type definitions, state definitions,
value definitions, operation definitions, def expression and block
statement). In IFAD VDM-SL an optional semicolon can be used also in the
end.
b) Post conditions in explicit function and operations can not be defined,
that is an IFAD VDM-SL extension.
c) The body of an explicit function must be defined ("is not yet specified"
is an IFAD VDM-SL extension.
d) Empty sets and empty sequences can not be used directly as patterns, this
is an IFAD VDM-SL extension.
e) Tuple selection must be done by pattern-matching ( .#N is an IFAD VDM-SL
extension).
f) The symbol used for total function is "-t>" while in IFAD VDM-SL is "+>".
II. Unimplemented features of ISO VDM-SL
a) Comments can apper between "annotation" and "end annotation".
b) Identifier with a hook, if an identifier coincides with a keyword then it
is preceded by $ (dollar sign).
c) Interchange syntax adds new keywords that are not specified in the
"keyword" rule nor in context-free syntax (to be rejected as an
Identifier).
d) In ISO VDM-SL tagged types (the ones that are defined with ::) are
constructed using only its name. This creates an ambiguity that can not
be solved, between record constructor and apply expression (although no
error was reported). To correct this, a record constructor has the same
syntax as IFAD VDM-SL "mk_" Name "(" ExpressionList? ")"
e) The rule Function Type Instantiation of the Applicators Family was not
introduced in the desambiguation filters because it did not caused any
ambiguity.
f) IsExpressions rule were changed because of an ambiguity between Apply. For
this reason, an IsDefinedTypeExpression was defined as:
"is_" Identifier "(" Identifier ")", in which the "is_" part was added to
disambiguate with Apply. This was the same strategy adopted by IFAD VDM-SL.
g) All the rules that use Expression | CallStatement have an ambiguity, this
is because CallStatement have the same syntax as the Expression Apply.
This happens in the following ISO rules: EqualsDefinition,
AssignmentDefinition and AssignStatement.
IFAD solution was to only allow Expression in the three rules, removing
this way the ambiguity. But what does it means semanticaly?
This problem does not arise when the lhs of the apply is not a Name or
when the call statement uses "using" state designator. The question is,
The apply having a lhs with a name is semanticaly equivalent to the call
statement without using state designator?
My solution was to prefer Expression whenever there is an ambiguity, which
chooses Expression in most of the cases. This must be reviewed later.
III. Notes about grammar features
a) The iterate ("**") can be used in more than one context:
- It was found that can be used in arithmetic operations as power of a
number, for instance: 3 ** 2 = 9.
- It can be used as map iteration, for instance:
{ 1 |-> 2, 2 |-> 3, 3 |-> 4, 4 |-> 1 } **3 =
{ 1 |-> 4, 2 |-> 1, 3 |-> 2, 4 |-> 3 }.
- it can be used as function iteration which applies a function n times
to an argument, for instance: (f ** 4) 2 = f(f(f(f(2)))
b) The composition ("comp") can be used in two contexts:
- map composition
- function composition
A problem was found in using "comp" with "**". By testing IFAD VDMTools
it was found that the two operators have right associativity between
them. This was tested for function composition and function iteration,
but not for map composition and map iteration.
|