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?

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.

It's important to realize that KnuckleDragger 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

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

>>> notDiv3
Lemma: case_n_mod_3_eq_0
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Result:                               Q.E.D.
Lemma: case_n_mod_3_eq_1
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Step: 6                               Q.E.D.
Result:                               Q.E.D.
Lemma: case_n_mod_3_eq_2
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Step: 6                               Q.E.D.
Result:                               Q.E.D.
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

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,Idle,Ready,Critical,Critical,Critical,Idle,Ready,Critical]
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!

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.

Check if the symbolic value is nothing.

>>> isNothing (sNothing :: SMaybe Integer)
True

>>> isNothing (sJust (literal "nope"))
False

The symbolic Nothing.

>>> sNothing :: SMaybe Integer
Nothing :: SMaybe Integer

We cannot push an existential through conjunction. We have:

>>> existsConjunctionNot `catch` (\(_ :: SomeException) -> pure ())
Lemma: existsConjunctionNot
*** Failed to prove existsConjunctionNot.
Falsifiable. Counter-example:
p :: T -> Bool
p T_1 = False
p _   = True

q :: T -> Bool
q T_1 = True
q _   = False

In this case, we again have a predicate That disagree at every point, providing a counter-example.

We cannot push a universal through a disjunction. We have:

>>> forallDisjunctionNot `catch` (\(_ :: SomeException) -> pure ())
Lemma: forallConjunctionNot
*** Failed to prove forallConjunctionNot.
Falsifiable. Counter-example:
p :: T -> Bool
p T_2 = True
p T_0 = True
p _   = False

q :: T -> Bool
q T_2 = False
q T_0 = False
q _   = True

Note how p assigns two selected values to True and everything else to False, while q does the exact opposite. So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds a model with two distinct values, as one would have sufficed. But it is still a valud model.)