tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 8 forks source link

Adding universal quantification to asserts #228

Closed sidprasad closed 7 months ago

sidprasad commented 7 months ago

Universal assertions of the form:

assert all r1 : Node | isRoot[r1] is necessary for isDirectedTree assert all r1, r2 : Node | isRoot[r1] is necessary for q[r2] assert all a,b : N1, c,d : N2 | p[a,b] is sufficient for s[c,d]

are now supported.

Issues: