overture
overture copied to clipboard
Interpreter crash during model initialization does not get reported
If you execute the VDM-SL spec below (using DEFAULT`f() as the entry) then the interpreter dies silently and no result is output to the console.
The problems happens during the initialization of the model where the interpreter tries to compute all members for the expression "set of A" which is the power-set of the type A. Since type A has (3_3) * (3_3) = 81 members the number of members for "set of A" are 2^81, which becomes too much for the interpreter to handle.
types
T = <C> | <B> | <A>;
A = (T * T) * (T * T);
values
xs = let s: set of A in s;
functions
f: () -> nat
f() == 1;
This is a side effect of #136