Closed pglvdm closed 10 years ago
We need @joey-coleman to check what the rule is for static stuff in cml (also related to a current parser issue).
I think that static is unsupported in cml. Try the same model using an instance of math. I think that it will work.
Sent from my iPhone
On 29/05/2014, at 09.14, pglvdm notifications@github.com wrote:
If one makes a CML model like:
process Test = begin
state reg : real
operations
operations
INIT : () ==> () INIT() == reg := MATH`cos(0)@ INIT()
end with a CML version of the standard MATH library which will look like:
class MATH = begin
-- Overture STANDARD LIBRARY: MATH
-- Standard library for the Overture Interpreter. When the interpreter -- evaluates the preliminary functions/operations in this file, -- corresponding internal functions is called instead of issuing a run -- time error. Signatures should not be changed, as well as name of -- module (VDM-SL) or class (VDM++). Pre/post conditions is -- fully user customisable. -- Dont care's may NOT be used in the parameter lists.
functions
public sin:real +> real sin(v) == is not yet specified
post abs RESULT <= 1public cos:real +> real cos(v) == is not yet specified post abs RESULT <= 1
public tan:real -> real tan(a) == is not yet specified pre cos(a) <> 0
public cot:real -> real
cot(a) == is not yet specified -- Could also be: 1/tan(r) pre sin(a) <> 0public asin:real -> real asin(a) == is not yet specified pre abs a <= 1
public acos:real -> real acos(a) == is not yet specified pre abs a <= 1
public atan:real +> real atan(v) == is not yet specified
public acot:real +> real acot(a) == atan(1/a) pre a <> 0
public sqrt:real -> real sqrt(a) == is not yet specified pre a >= 0
public pi_f:() +> real pi_f () == is not yet specified
operations
public srand:int ==> () srand(a) == let - = MATH`srand2(a) in Skip pre a >= -1
public rand:int ==> int rand(a) == is not yet specified
public srand2:int ==> int srand2(a) == is not yet specified pre a >= -1
functions
public exp:real +> real exp(a) == is not yet specified
public ln:real -> real ln(a) == is not yet specified pre a > 0
public log:real -> real log(a) == is not yet specified pre a > 0
public
fac:nat -> nat1 fac(a) == is not yet specified pre a < 21 -- The limit for 64-bit calculationsvalues public pi = 3.14159265358979323846
end it works perfectly from a type checking perspective. However, if one try to interpret the model one gets an error message like:
Error 4034: Name 'MATH`cos(nat)' not in scope in 'cos' (C:\TEMP\SymphonyIDE\workspace\Test\Test.cml) at line 11:25 at in 'cos' (C:\TEMP\SymphonyIDE\workspace\Test\Test.cml) at line 11:25 which indicates to me that definitions from the VDM libraries can be used from a type checking perspective but not from an interpreter perspective. If this could be fixed it would be possible to add the standard VDM libraries to CML models in exactly the same way. Wauh!
— Reply to this email directly or view it on GitHub.
Yes indeed cos works if I make a new instance of it. But still it would be an advantage if we could get these working in a static setting.
I seem to recall that the object semantics presented in D23.4/D23.5 does not have a the notion of static access, but I'd have to re-read a chunk of it to confirm that.
Assigning to me so I remember to look into it.
I've checked D23.4c on the OO semantics, and I think we have no model for static
(class-level) attributes nor operations. So, as far as I see, we can do what we like.
If one makes a CML model like:
with a CML version of the standard MATH library which will look like:
it works perfectly from a type checking perspective. However, if one try to interpret the model one gets an error message like:
which indicates to me that definitions from the VDM libraries can be used from a type checking perspective but not from an interpreter perspective. If this could be fixed it would be possible to add the standard VDM libraries to CML models in exactly the same way. Wauh!