For example, I want to cast nat to seq of char in VDM++.
In the code below, I want operation setValueOfX to return "X is {value of q}"
, if q is of type nat and q < 3.
class A1
instance variables
private x : nat := 0;
operations
public setValueOfX : nat ==> seq of char
setValueOfX(q) ==
(
if is_nat(q) and q < 3
then
(
x := q;
-- The following line doesn't work
-- return "X is " ^ q;
)
else
return "Invalid value! Value of x must be more than 0 and less than 3.";
);
end A1
I've tried using ^
but I got the following error:
Error[207] : Rhs of '^' is not a sequence type
act : nat
exp : ( seq1 of # | [] )
No, you can't implicitly convert values like that in VDM.
If you just want to see the result in a textural form, you could look at the IO library, which lets you "print" a mixture of types to the console. Alternatively, if you must return a string, you could specify a function that converts a nat to a decimal string, and the return "Result is" ^ nat2str(q).