some key verifications constructs:
- requires (pre-condition)
- ensures (post-condition)
- we could generalize pre- and post- by saying that the 'requires' is a hypothetical logical statement bound to some program location, and then saying that the 'ensures' is just an assertion that if that hypothetical was true at its location, then this other thing is true; but i kind of like having 'require/ensure' modal sigils
- assert (point condition)
- ipromise (an assertion that cannot be proved, but that the programmer promises is true; this is perhaps a modal modifier to any of these; perhaps we just prepend whatever the 'ensures' sigil is? or postpend a '?'?)
- invariant (loop invariant; true at the beginning, and true in each subsequent iteration if true in each previous iteration)
- note: isn't this just an assertion with a specific suggested method of finding a proof? so couldn't we leave this out?
- forall (to introduce variables inside the previous ones) (mb 'forall i :: (rest of logical boolean expression)')
- decreases (something that decreases over each iteration of a loop; used to prove loop termination)
- should we also allow structural recursion?
- mbnonterminating (used when a proof of termination is not desired)
to have 'proofs', just have a sequence of 'asserts' that follow in one inference step from previous in-scope 'asserts' and in-scope 'requires' and in-scope invariants
note that short-circuit boolean implication (and short-circuit AND) is very useful here for sayings like eg: forall i : int :: (0 <= i && i < len(arr)) -> predicate(arr[i])) (where '->' is short-circuit boolean implication and 'predicate(arr[i])' is something that you are saying is true for each element in the array)
---