Whiley / WhileyCompiler

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

Check for Static Field Assignment #1120

Closed DavePearce closed 2 years ago

DavePearce commented 2 years ago

This should not compile:

int GLOBAL = 0

function f():
    GLOBAL = 1
DavePearce commented 2 years ago

Have implemented this, but it remains to handle these cases:

int x = 0

method main():
   assert x == 0

Currently above does not compile, though it seems reasonable to assume that it would.

DavePearce commented 2 years ago

Presumably a loop invariant would also be able to access it.

DavePearce commented 2 years ago

Also this should be valid I suppose as well:

int var = 1

method m()
requires var >= 0:
   ...