|
|
|
The CONVECS team is pleased to announce
that version 3.9 of the TRAIAN compiler for LOTOS NT is available.
With TRAIAN 3.9, the convergence between LOTOS NT and LNT is nearly complete. Measured on a test suite of 13,500+ correct LNT programs totalling more than 9 million non-blank lines of LNT code, TRAIAN 3.9 syntactically accepts 100% of these programs (whereas TRAIAN 3.8 accepted 97.4% of them) and semantically accepts 89.3% of them at the moment (this percentage is expected to increase in the near future).
For many years, TRAIAN has been used to develop compilers, including those of the CADP toolbox. At present, it is also intensively used to check LNT specifications of concurrent systems, allowing to catch mistakes not detected by the "lightweight" approach of the LNT2LOTOS translator.
TRAIAN 3.9 brings twelve language changes, ten static-semantics changes, seven compiler changes, two release changes, and four bug fixes (see below their description).
function # (x: Nat) : Nat is
return x + 1
end function
See item 455 in the HISTORY.txt file.
For instance, the following code fragment "F1 F2 V" (where F1 and F2 are special unary operators and V an expression) is no longer accepted, and should be written either "F1 (F2 V)" or "F1 (F2 (V))". For instance, "- * # P" must now be written "- (* (#P))".
It is also forbidden to mix, without parentheses, a unary operator, which is a prefix notation, and the "of" operator, which is a postfix notation. Concretely, "F V of T" is now rejected as ambiguous, and should be written either "(F V) of T" or "F (V of T)". This enables one to better distinguish between, e.g., "(- 128) of BYTE" and -(128 of BYTE). See item 462 in the HISTORY.txt file.
PRINT (- -1) PRINT ((- -1) of bool)From now on, one should write:
PRINT (- (-1)) PRINT ((- (-1)) of bool)which is more readable and better expresses the user's intent. See item 463 in the HISTORY.txt file.
Note that such parentheses are not required between unary "+" or unary "-" and numeric constants to obey longstanding mathematical traditions.
Also, the following pattern "X * any T + Y", which was formerly accepted and parsed as "(X * any) T (+ Y)", is now rejected with a syntax error: "(" is inserted before "Y". We believe that the new behaviour is more intuitive and avoids confusion.
Because of this change, some correct LOTOS NT programs may become incorrect and must by updated manually to be accepted by TRAIAN 3.9. See item 467 in the HISTORY.txt file.
=, <> : BOOL, BOOL : BOOL
=, <> : NAT, NAT : BOOL
=, <> : INT, INT : BOOL
=, <> : REAL, REAL : BOOL
=, <> : CHAR, CHAR : BOOL
=, <> : STRING, STRING : BOOL
These functions provide alternate notations: "=" is a synonym for "==" and
"<>" is a synonym for "!=".
See item 474 in the HISTORY.txt file.
MIN : NAT, NAT -> NAT MAX : NAT, NAT -> NAT MIN : INT, INT -> INT MAX : INT, INT -> INT GCD : [ZERO_DIVISION] NAT, NAT -> NAT GCD : NAT, NAT -> NAT SCM : [ZERO_DIVISION] NAT, NAT -> NAT SCM : NAT, NAT -> NATThis may cause name clashes, e.g., if functions MIN or MAX are already defined with the same profiles in a LOTOS NT program. In such case, the solution is to rename or comment out those functions. See item 475 in the HISTORY.txt file.
function F [E : none] (X: Bool) : Bool is
raise E;
return (not (X))
end function
now triggers a warning:
function with result but no normal terminationSee item 454 in the HISTORY.txt file.
error: missing exceptional event in field access
an exception is needed in value:
V.F
since V has type T, not all constructors of which have
a field F
From now, these expressions are accepted at compile-time, but may raise an
UNEXPECTED event at run-time, under the assumptions that
V.F is equivalent to V.[UNEXPECTED] Fand that
V.{F->...} is equivalent to V.[UNEXPECTED] {F->...}
See item 457 in the HISTORY.txt file.
function with "out" parameter(s) but no normal terminationwhen the body of a function declared with "out" parameters contains no "return" statement, but raises (e.g., using a "raise" instruction) an event declared in the function profile. Indeed, raising such event can be considered as a normal (or admissible) way of terminating for this function. See item 458 in the HISTORY.txt file.
Therefore, the LOTOS names used in the !implementedby pragmas of LOTOS NT functions may be identical, but they must obey a new rule not to create name clashes. Two LOTOS NT functions may have the same LOTOS name provided that their profiles (argument types and result types) are different. Otherwise, the following error message will be emitted:
pragma !implementedby "LOTOS:N" already used for same-profile function F at ...Conversely, the unicity rule remains for C identifiers present in !implementedby "C:..." pragmas, and also for LOTOS type identifiers present in !implementedby "LOTOS:..." pragmas attached to LOTOS NT types. Violations of the latter rule trigger the following error message:
pragma !implementedby "LOTOS:N" already used for type T at ...See item 459 in the HISTORY.txt file.
function F:int is
trap
exception X is null
in
return 0
end trap
end function
that were previously rejected with the following message:
error: function F may terminate without returning a valueSee item 464 in the HISTORY.txt file.
error: function with result but looping infinitely error: function with "out" parameter but looping infinitelyFor instance, the following LOTOS NT programs are rejected with warning and error messages:
function F (in var X : BOOL) : BOOL is
while true loop
X := not (X)
end loop;
return X
end function
function F (in var X : Int) : Int is
trap
exception E is
return X
in
while true loop
X := X - 1
end loop;
raise E
end trap
end function
Infinite loops are rejected even if they occur in dead code. For instance,
the following LOTOS NT program is rejected:
function F [E: none] (X: BOOL, out Y: BOOL): BOOL is
trap
exception Z is
loop null end loop
in
raise E
end trap;
return X or Y
end function
The rationale is that infinite loops in functions are blatantly violating the
semantics of LOTOS NT, which assumes that expressions are evaluated atomically
and instructions are executed atomically. Even if non-termination cannot be
detected in the general case, the increased severity of TRAIAN aims at
discouraging users to disseminate infinite loops in their code, even in
dead code areas.
See item 465 in the HISTORY.txt file.
The former semantics prevented the user from defining specific "==" and "!=" functions for certain types, as previous versions of TRAIAN would report function name clashes in such case.
Because of this change, many LOTOS NT programs formely accepted may be rejected by TRAIAN 3.9. An easy solution is to add "with ==, !=" in type definitions or, only once, in the module header.
The C code generated by TRAIAN has been modified to always contain the equality comparison function, even when no "with ==" clause is present in the LOTOS NT code. See item 476 in the HISTORY.txt file.
TEST.lnt: "eval" before function calls in instructions is deprecated and should be removed (2 occurrences found)now displays as follows:
TEST.lnt:48 "eval" before function calls in instructions is deprecated and should be removed (2 occurrences found)thus informing the user that the first occurrence appears at line 48. See item 446 in the HISTORY.txt file.
error: TEST.lnt:5: loop L is already defined at TEST.lnt:4 warning: TEST.lnt:967: useless assignment to DEF warning: TEST.lnt:1042: variable Z never usednow display as follows:
TEST.lnt:5: error: loop L is already defined at TEST.lnt:4 TEST.lnt:967: warning: useless assignment to DEF TEST.lnt:1042: warning: variable Z never usedAlso, a few messages have been modified to add missing colons. See item 450 in the HISTORY.txt file.
TEST.lnt:313: error: too large natural constant 10000000000000000000000000000or
TEST.lnt:16777218: limitation: too many lines (maximum is 16777215)See item 452 in the HISTORY.txt file.
warning: missing file TEST.tnt for external types error: syntax error in ".lnt" filenow display as follows:
traian: warning: missing file TEST.tnt for external types traian: error: "TEST.lnt" is syntactically incorrect(notice that the latter message was made more informative). See item 453 in the HISTORY.txt file.
error: variable or function F is not definedif it is certain that F denotes a function, not a variable. The following rules are used: if F is followed with empty parentheses "()", or if the identifier of F is not that of a variable (e.g., 0X0123_456), then F is surely a function and TRAIAN issues the following error message:
error: function F is not definedSee item 469 in the HISTORY.txt file.
Also, three libraries borrowed from CADP (BIT.lnt, OCTET.lnt, and OCTETVALUES.lnt) have been added in the "lib" directory of the TRAIAN distribution. See item 470 in the HISTORY.txt file.
At present, C code generation is not yet available for these types (an error message is triggered if a LOTOS NT program contains such types). However, all the aforementioned checks are sufficient for the "-analysis" option of TRAIAN, which can thus be used to check LNT specifications of concurrent systems. See item 479 in the HISTORY.txt file.
function F (out X:nat) : BOOL is
loop L in
X := 0;
return true
end loop
end function
and:
function F (out X:nat) : BOOL is
loop K in
loop L in
X := 0;
break L
end loop;
return false
end loop;
return true
end function
with the following error message:
function F may return without assigning parameter XFrom now on, such programs are accepted by TRAIAN. See item 451 in the HISTORY.txt file.
function F (out R : Nat) is
var I : Nat in
I := 0;
loop
case I in
any Nat ->
if I == 1 then
R := 1;
return
end if;
I := I + 1
end case
end loop
end var
end function
to be rejected with the error message:
function F may return without assigning parameter RFrom now on, such programs are accepted by TRAIAN. See item 461 in the HISTORY.txt file.
function F [E : none] (in var N : NAT) : NAT is
var R : NAT in
for R := 1 while true by N := N -[E] 1 loop
if N > 0 then
R := R * N
end if
end loop;
return R
end var
end function
with an error message:
function with result but looping infinitelyFrom now on, this code is accepted by TRAIAN. See item 466 in the HISTORY.txt file.
redundant clause "with F" for type T (already present for the module)and a fatal error:
function F is already defined with the same profile at ...From now on, only the warning is emitted. See item 477 in the HISTORY.txt file.
TRAIAN will continue to evolve, our goal being to merge LOTOS NT and LNT
in one single language.
TRAIAN 3.9 can be freely downloaded from the TRAIAN Web Page located at: