VDD: Two Functions with a Non-Intersection Spec

This tutorial extends the VDD flow to two functions plus a global non-intersection constraint. We again start with abstract contracts and then refine into implementations. The global claim uses a universal quantifier so one contract can cover every integer input.

1) Declaration-only spec

The spec declares two pure abstract functions and a noCross obligation. The noCross postcondition states that the functions stay at least 1 unit apart for every integer input. While these declarations remain abstract, their contracts are assumptions; after refinement, the bodies must prove those contracts.

Source: snippets/equation_system_sat.mo

module {
  public pure abstract func conditionalBounds(x : Int) : Int
    ensures x == 5 ==> result > 10;
    ensures x == 8 ==> result < 5;
    ensures x == 12 ==> result > 14;
    ensures x == 14 ==> result < 5;
    ensures x == 16 ==> result > 18;
    ensures (x == 5 or x == 12 or x == 16) ==> result % 2 == 1;
    ensures (x == 8 or x == 14) ==> result % 2 == 0;
    ensures (x == 5 or x == 12 or x == 16) ==> result * result > x * x;
    ensures (x == 8 or x == 14) ==> result * result <= 16;

  public pure abstract func alternateEquation(x : Int) : Int
    ensures x == 6 ==> result < -5;
    ensures x == 9 ==> result > 11;
    ensures x == 13 ==> result > 12;
    ensures x == 15 ==> result >= 11;
    ensures x == 17 ==> result > 77;
    ensures (x == 6 or x == 9 or x == 17) ==> result % 2 == 0;
    ensures (x == 13 or x == 15) ==> result % 2 == 1;
    ensures x == 9 ==> result >= conditionalBounds(x) + 2;
    ensures x == 15 ==> result >= conditionalBounds(x) + 10;

  public abstract func noCross() : ()
    ensures forall<Int>(pure func (t : Int) : Bool =
      (alternateEquation(t) - conditionalBounds(t)) * (alternateEquation(t) - conditionalBounds(t)) >= 1);
}

Verify the declaration. Denied ranges for the two functions use different x positions to keep the plots readable:

2) Refine into implementations

We keep the original interpolation for conditionalBounds and refine alternateEquation by adding a quadratic shift. This avoids the “constant offset” shortcut while still satisfying the separation constraint.

Source: snippets/equation_system_full_body_sat.mo

module {
  public pure func conditionalBounds(x : Int) : Int
    ensures x == 5 ==> result > 10;
    ensures x == 8 ==> result < 5;
    ensures x == 12 ==> result > 14;
    ensures x == 14 ==> result < 5;
    ensures x == 16 ==> result > 18;
    ensures (x == 5 or x == 12 or x == 16) ==> result % 2 == 1;
    ensures (x == 8 or x == 14) ==> result % 2 == 0;
    ensures (x == 5 or x == 12 or x == 16) ==> result * result > x * x;
    ensures (x == 8 or x == 14) ==> result * result <= 16;
  {
    let term1 = 11 * (x - 8) * (x - 12) * (x - 14) * (x - 16) / 2079;
    let term2 = 15 * (x - 5) * (x - 8) * (x - 14) * (x - 16) / 224;
    let term3 = 19 * (x - 5) * (x - 8) * (x - 12) * (x - 14) / 704;
    term1 + term2 + term3
  };

  public pure func alternateEquation(x : Int) : Int
    ensures x == 6 ==> result < -5;
    ensures x == 9 ==> result > 11;
    ensures x == 13 ==> result > 12;
    ensures x == 15 ==> result >= 11;
    ensures x == 17 ==> result > 77;
    ensures (x == 6 or x == 9 or x == 17) ==> result % 2 == 0;
    ensures (x == 13 or x == 15) ==> result % 2 == 1;
    ensures x == 9 ==> result >= conditionalBounds(x) + 2;
    ensures x == 15 ==> result >= conditionalBounds(x) + 10;
  {
    conditionalBounds(x) + 1 + (x - 6) * (x - 6) / 9
  };

  public func noCross() : ()
    ensures forall<Int>(pure func (t : Int) : Bool =
      (alternateEquation(t) - conditionalBounds(t)) * (alternateEquation(t) - conditionalBounds(t)) >= 1);
  {
  };
}

Verify the implementation, then plot both functions against their denied ranges:

Note: the non-intersection guarantee is for integer inputs (Int). If you need continuous non-intersection, the spec must model real-valued behavior instead; Sector9 proves the semantics you encode, not an implicit plotting interpretation.