VDM Tools - FAQ

Error / Warnings

Warning[412]: "..." is recursive but does not have a measure defined: A measure must be added to the function to prove that it terminates. The function can work without but need to be proven.

Error[?] Call Statement must have an argument list: You have properly forgotten a return in your operation.

 

 

 

Special commands

objects -a Print all objects can be used if a objrefXXX isn't displayed
$$ Last result
state -r list all objects
state -d objectId display a object
popd Remove last action from stack. If error in interpreter popd and then continue.