Subversion

2lt

?curdirlinks? - Rev 1

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

Theme by Vikram Singh | Powered by WebSVN v2.3.3