Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
217 stars 36 forks source link

Runtime Checking of Type Invariants #1145

Closed DavePearce closed 2 years ago

DavePearce commented 2 years ago

Test 001177:

type Point is {int x, int y} where x < y

method test(&Point ptr):
    int x = ptr->x
    // break invariant
    ptr->x = 1
    // restore invariant
    ptr->x = x

public export method test():
   test(new {x:1,y:2})
   test(new {x:0,y:1})

This fails statically because of the temporary invariant failure on line 6. However, the interpreter misses this.

Unfortunately, its not entirely clear to me how we are supposed to manage expected invariants like this? In this case, we can just examine the contents of ptr.