vdmj

vdmj copied to clipboard

@spec(name[, weight]) annotation

2

Nick, I wanted to suggest a new annotation. I thought to implement it in VDM_Toolkit but then wanted to share it here for thoughts/comments (or warnings!). :-) A while ago...

leouk

See https://github.com/jonaskrask/vdm-vscode/issues/62 We need to separate the condition from the logged trace value and do multiple checks.

nickbattle

Measures for inline function definitions don't work

1

Consider the following: ``` f: nat -> nat f(x) == let g: nat -> nat g(a) == if a = 0 then 0 else a + g(a-1) pre a >...

nickbattle

The following produces a stack overflow: ``` types T = R; R = T; Parsed 1 module in 0.054 secs. No syntax errors java.lang.StackOverflowError Error 3050: Type 'T' is infinite...

nickbattle

Consider the following: ``` f[@T]: @T * @T -> nat f(a, b) == a + b pre is_real(a) and is_real(b); ``` This is type clean, and allows a pair of...

nickbattle

ClassMapper terminates JVM on error

22

The classmapper contains both System prints and `System.exit` call which makes it hard to embed into other software. Before this class only raised error messages while it currently both prints...

lausdahl

Provide launch and tasks files

8

I suggest adding a `launch.json` and `tasks.json` to the project that easily allows newcomers to get started with debugging/building the project in VSCode.

mortenhaahr

@LoopInvariant annotation

3

For loop statements, a loop invariant annotation would be useful for further proof of termination and translation to Isabelle.

leouk