search

flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Add doc and test for the fact that a quantifier's bindings can be empty #106

Closed wilcoxjay closed 1 year ago

wilcoxjay commented 1 year ago

This PR adds a bit of documentation and a test to call out the fact that a Term::Quantifier's list of bindings can be empty.

Not saying I think it should work this way, but this is how the code works. The parser supports it, and at least some paths in the code (eg semantics::eval_assign) handle this case.

vmwclabot commented 1 year ago

@wilcoxjay, you must sign every commit in this pull request acknowledging our Developer Certificate of Origin before your changes are merged. This can be done by adding Signed-off-by: John Doe <john.doe@email.org> to the last line of each Git commit message. The e-mail address used to sign must match the e-mail address of the Git author. Click here to view the Developer Certificate of Origin agreement.

vmwclabot commented 1 year ago

@wilcoxjay, you must sign every commit in this pull request acknowledging our Developer Certificate of Origin before your changes are merged. This can be done by adding Signed-off-by: John Doe <john.doe@email.org> to the last line of each Git commit message. The e-mail address used to sign must match the e-mail address of the Git author. Click here to view the Developer Certificate of Origin agreement.