proj-oot-ootVerificationThoughts

some key verifications constructs:

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)

---