tnelson / Forge

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

Change misleading `is theorem` to `is checked` #276

Closed tnelson closed 3 weeks ago

tnelson commented 3 weeks ago

The phrase "is theorem" in a test implies that there is some sort of complete check being done, but by default Forge only checks up to a bound. Thus, we will replace "is theorem" with "is checked" (which is not ideal but is at least not actively misleading).

Existing models that use is theorem will receive an error letting them know that the keyword is disabled, but may be re-added at such time as Forge incorporates a solver backend that is complete.