Skip to main content

Biconditional (<==>)

The biconditional operator expresses logical equivalence: "A if and only if B". Like ==>, it is a proof/specification operator rather than a general runtime boolean operator.

Syntax​

condition1 <==> condition2

The expression a <==> b is true when both sides have the same truth value:

  • Both a and b are true
  • Both a and b are false

It is logically equivalent to (a ==> b) and (b ==> a), or equivalently (a and b) or (not a and not b).

<==> is accepted in ghost contexts such as contracts, static assert, loop:invariant, pure functions, and lemmas. Runtime code should use a == b for boolean equality.

Using Biconditional in Assertions​

The biconditional is useful for verifying that two expressions are logically equivalent:

persistent actor IffOperator {
  public func equalZero(x : Int) : async Bool
    ensures result == (x == 0);
  {
    assert (x == 0 <==> (x <= 0 and x >= 0));
    x == 0
  };
}

This assertion proves that x == 0 is equivalent to x being both less-than-or-equal-to zero and greater-than-or-equal-to zero.

Using Biconditional in Contracts​

Use <==> in postconditions to express that two conditions are equivalent:

public func isEmpty(arr : [Nat]) : async Bool
  ensures result <==> arr.size() == 0;
{
  arr.size() == 0
};

This contract states that the return value is true exactly when the array is empty.

Common Patterns​

Verifying Logical Laws​

The biconditional is ideal for verifying logical equivalences like the contrapositive:

public func contrapositive(p : Bool, q : Bool) : Bool
  ensures result == (not p or q);
  ensures (p ==> q) <==> (not q ==> not p);  // Contrapositive law
{
  not p or q
};

De Morgan's Laws​

Verify that boolean transformations preserve meaning:

public func deMorgan1(a : Bool, b : Bool) : Bool
  ensures result == not (a and b);
  ensures result <==> (not a or not b);  // De Morgan
{
  not (a and b)
};

Characterizing Return Values​

Express the exact condition under which a function returns true:

public func isPositive(x : Int) : async Bool
  ensures result <==> x > 0;
{
  x > 0
};

Relating Runtime and Specification​

Use biconditional to connect runtime boolean expressions with their specification forms:

public func biImplicationLogic(x : Bool, y : Bool) : Bool
  ensures result == ((not x or y) and (not y or x));  // Runtime form
  ensures (x <==> y) ==> result;  // Specification form
{
  (not x or y) and (not y or x)
};

Precedence​

The <==> operator has the same precedence as ==>, which is lower than and and or:

a and b <==> c and d    // Parsed as: (a and b) <==> (c and d)

Use parentheses for clarity when mixing with implication:

(a <==> b) ==> c   // If a and b are equivalent, then c
a <==> (b ==> c)   // a is equivalent to (b implies c)

The operator is non-associative:

// This is rejected:
// a <==> b <==> c

// Use explicit grouping:
(a <==> b) and (b <==> c)   // a, b, and c are all equivalent

Truth Table​

aba <==> b
falsefalsetrue
falsetruefalse
truefalsefalse
truetruetrue

Comparison with Equality​

For boolean values, a <==> b and a == b produce the same result. However, <==> is preferred in specifications because:

  • It emphasizes logical equivalence rather than value comparison
  • It reads naturally: "a if and only if b"
  • It signals intent to verify a logical relationship

Summary​

  • a <==> b means "a if and only if b" (logical equivalence)
  • True when both sides have the same truth value
  • Use to verify logical laws, characterize return values, and express equivalences
  • Only available in ghost/specification contexts
  • Same precedence as ==>, lower than and/or, non-associative