Whiley / WhileyCompiler

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

Runtime Type Checking of Cyclic Assignment #1148

Open DavePearce opened 2 years ago

DavePearce commented 2 years ago

(see also #1145)

000497 fails because it attempts to check (at runtime) the invariant of a cyclic type:

type Cyclic is { null|&Cyclic ptr, int data }

public export method test():
    &Cyclic p = new {ptr:null, data: 0}
    &Cyclic q = new {ptr:p, data: 0}
    // Make it cyclic!
    p->ptr = q
    //
    assert p != q
    assert p->data == q->data

This is certainly problematic!