not package:sbv

The connective not negates a statement

Uninterpreted logical connective not

Is the character not in the string?

>>> prove $ \c s -> c `elem` s .<=> sNot (c `notElem` s)
Q.E.D.

notElem e l. Does l not contain the element e?

>>> prove $ \(x :: SList Integer) -> x `notElem` []
Q.E.D.

Match nothing, universal rejector.

>>> prove $ \(s :: SString) -> sNot (s `match` nothing)
Q.E.D.

Test for non-membership.

>>> prove $ \x -> x `notMember` observe "set" (singleton (x :: SInteger))
Falsifiable. Counter-example:
s0  =   0 :: Integer
set = {0} :: {Integer}

>>> prove $ \x (s :: SSet Integer) -> x `notMember` (x `delete` s)
Q.E.D.

>>> prove $ \x -> x `notMember` (empty :: SSet Integer)
Q.E.D.

Our algorithm is correct, but it is not fair. It does not guarantee that a process that wants to enter its critical-section will always do so eventually. Demonstrate this by trying to show a bounded trace of length 10, such that the second process is ready but never transitions to critical. We have:

>>> notFair 10
Fairness is violated at bound: 10
P1: [Idle,Idle,Ready,Critical,Idle,Ready,Critical,Critical,Idle,Ready]
P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready]
Ts: [1,1,1,1,1,1,1,1,1,1]

As expected, P2 gets ready but never goes critical since the arbiter keeps picking P1 unfairly. (You might get a different trace depending on what z3 happens to produce!) Exercise for the reader: Change the validTurns function so that it alternates the turns from the previous value if neither process is in critical. Show that this makes the notFair function below no longer exhibits the issue. Is this sufficient? Concurrent programming is tricky!

It's important to realize that TP proofs in SBV neither check nor guarantee that the functions we use are terminating. This is beyond the scope (and current capabilities) of what SBV can handle. That is, the proof is up-to-termination, i.e., any proof implicitly assumes all functions defined (or axiomatized) terminate for all possible inputs. If non-termination is possible, then the logic becomes inconsistent, i.e., we can prove arbitrary results. Here is a simple example where we tell SBV that there is a function f with non terminating behavior. Using this, we can deduce False:

>>> noTerminationChecks
Axiom: bad
Lemma: noTerminationImpliesFalse
Step: 1 (bad @ (n |-> 0 :: SInteger)) Q.E.D.
Result:                               Q.E.D.
[Proven] noTerminationImpliesFalse :: Bool

Prove that 2n^2 + n + 1 is not divisible by 3. We have:

>>> notDiv3
Lemma: notDiv3
Step: 1 (3 way case split)
Step: 1.1                           Q.E.D.
Step: 1.2                           Q.E.D.
Step: 1.3                           Q.E.D.
Step: 1.Completeness                Q.E.D.
Result:                               Q.E.D.
[Proven] notDiv3 :: Ɐn ∷ Integer → Bool

>>> runTP nothingBetweenZeroAndOne
Lemma: nothingBetweenZeroAndOne         Q.E.D.
[Proven] nothingBetweenZeroAndOne :: Ɐm ∷ Nat → Bool

Class of things that we can logically negate

Annotate for the metric space, to clarify the new name. If this result is not identity, we will add an sObserve on the original.

Negation of a quantified formula. This operation essentially lifts sNot to quantified formulae. Note that you can achieve the same using sNot . quantifiedBool, but that will hide the quantifiers, so prefer this version if you want to keep them around.

Symbolic boolean negation

Symbolic negated membership test.

Bitwise complement.

Inequality.

Field recognizer predicate.

Symbolic version of the constructor Nothing.

Make sure self-application cannot be typed.

>>> selfAppNotWellTyped
Unsatisfiable

We get unsatisfiable, indicating there's no way to come up with an environment that will successfully assign a type to the term x -> x x.