Whiley / WhileyCompiler

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

Runtime Multiple Assignment #1147

Closed DavePearce closed 2 years ago

DavePearce commented 2 years ago

000443 generates a type invariant failure:

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

public export method test():
    Rec r = {x:0,y:1}
    // Increment both by one
    r.x,r.y = r.x+1,r.y+1
    // Check!
    assert r == {x:1,y:2}