Skip to main content

Combining Conditions

Building complex specifications from simple predicates using logical operators.

Operator Summary​

Sector9 provides these logical operators for specifications:

OperatorNameMeaning
notNegationTrue if operand is false
andConjunctionTrue if both operands are true
orDisjunctionTrue if at least one operand is true
==>ImplicationTrue if antecedent is false or consequent is true
<==>BiconditionalTrue if both operands have the same truth value

not, and, and or are ordinary boolean operators. ==> and <==> are ghost/specification operators: use them in contracts, static assertions, loop invariants, pure functions, and lemmas, but use if, and, or, not, or boolean equality in executable runtime code.

Precedence Rules​

Operators bind in this order (tightest to loosest):

  1. not (prefix, tightest)
  2. and
  3. or
  4. ==> and <==> (same level, loosest)

This means:

not a and b or c ==> d
// Parses as: (((not a) and b) or c) ==> d

a and b ==> c or d
// Parses as: (a and b) ==> (c or d)

Use parentheses liberally for clarity, especially in complex expressions.

Building Specifications​

Case Analysis​

Use implication to specify different cases:

public func absolute(x : Int) : async Int
  ensures x >= 0 ==> result == x;
  ensures x < 0 ==> result == -x;
{
  if (x >= 0) { x } else { -x }
};

Each ensures clause handles one case. The verifier proves both.

Conjunctive Postconditions​

Multiple ensures clauses are implicitly conjoined:

public func clamp(x : Int, lo : Int, hi : Int) : async Int
  entry_requires lo <= hi;
  requires lo <= hi;
  ensures result >= lo;
  ensures result <= hi;
  ensures x < lo ==> result == lo;
  ensures x > hi ==> result == hi;
  ensures lo <= x and x <= hi ==> result == x;
{
  if (x < lo) { lo }
  else if (x > hi) { hi }
  else { x }
};

All five postconditions must hold simultaneously.

Disjunctive Conditions​

Express "one or the other" with or:

public func classify(x : Int) : async Text
  ensures result == "negative" or result == "zero" or result == "positive";
{
  if (x < 0) { "negative" }
  else if (x == 0) { "zero" }
  else { "positive" }
};

Negation for Exclusion​

Use not to exclude impossible cases:

public func findPositive(arr : [Int]) : async ?Nat
  ensures result == null ==> not exists<Nat>(pure func(i : Nat) : Bool = i < arr.size() and arr[i] > 0);
{
  // ... search implementation
};

Complex Patterns​

Bounded Implications​

Combine range checks with implications:

public func lookup(arr : [Nat], idx : Nat) : async Nat
  entry_requires idx < arr.size();
  requires idx < arr.size();
  ensures result == arr[idx];
  ensures idx == 0 ==> result == arr[0];  // First element case
{
  arr[idx]
};

Nested Conditionals​

Express hierarchical logic with nested implications:

public func score(level : Nat, bonus : Bool) : async Nat
  ensures level < 5 ==> (bonus ==> result == 2);
  ensures level < 5 ==> (not bonus ==> result == 1);
  ensures level >= 5 ==> result == 3;
{
  if (level < 5) {
    if (bonus) { 2 } else { 1 }
  } else { 3 }
};

State Machine Transitions​

Verify valid state transitions:

type State = { #idle; #running; #stopped };

public func transition(current : State, event : Text) : async State
  ensures current == #idle and event == "start" ==> result == #running;
  ensures current == #running and event == "stop" ==> result == #stopped;
  ensures current == #stopped ==> result == #stopped;  // Terminal state
{
  switch (current, event) {
    case (#idle, "start") { #running };
    case (#running, "stop") { #stopped };
    case _ { current };
  }
};

Logical Laws in Specifications​

Verify well-known logical identities:

public func verifyDeMorgan(a : Bool, b : Bool, c : Bool) : async ()
{
  // De Morgan's laws
  assert not (a and b) <==> (not a or not b);
  assert not (a or b) <==> (not a and not b);

  // Contrapositive
  assert (a ==> b) <==> (not b ==> not a);

  // Distribution
  assert a and (b or c) <==> (a and b) or (a and c);
  assert a or (b and c) <==> (a or b) and (a or c);
};

Tips​

Start Simple​

Build complex conditions incrementally:

// Instead of one complex ensures:
// ensures (x > 0 and y > 0 ==> result > 0) and (x <= 0 or y <= 0 ==> result <= 0)

// Split into clear cases:
ensures x > 0 and y > 0 ==> result > 0;
ensures x <= 0 ==> result <= 0;
ensures y <= 0 ==> result <= 0;

Use Helper Predicates​

For repeated conditions, define pure helper functions:

pure func inRange(x : Int, lo : Int, hi : Int) : Bool {
  lo <= x and x <= hi
};

public func process(x : Int) : async Int
  entry_requires inRange(x, 0, 100);
  requires inRange(x, 0, 100);
  ensures inRange(result, 0, 100);
{
  // ...
};

Watch for Vacuous Truth​

Remember that false ==> anything is always true:

// This always passes, even if the function misbehaves when x < 0
ensures x >= 0 ==> result >= 0;

// To catch bugs for negative inputs, add:
ensures x < 0 ==> result < 0;

Summary​

  • Precedence: not > and > or > ==> / <==>
  • Multiple ensures clauses are conjoined (AND-ed together)
  • Use implication for case analysis in postconditions
  • Keep ==> and <==> in ghost/specification contexts
  • Split complex conditions into smaller, clearer parts
  • Define pure helper predicates for reusable conditions