// -----------------------------------------------------------------
// Comparing words in lexicgraphic order
// -----------------------------------------------------------------

val N:ℕ; // maximum word length
val C:ℕ; // number of characters
axiom notNull ⇔ C > 0;

type Index = ℕ[N];          // word positions (excluding N)
type Char  = ℕ[C-1];        // characters
type Word  = Array[N,Char]; // words
type Decision = ℤ[-1,1];    // -1:less, 0:equal, 1:greater

// word w has length n:
// only the first n positions of w contain information
pred length(w:Word, n:Index) ⇔
  ∀i:Index with n ≤ i ∧ i < N. w[i] = 0;

// d describes the lexicographic relationship between 
// word a of length an and word b of length bn
pred compares(a:Word, an:Index, b:Word, bn:Index, d:Decision) 
  requires length(a,an) ∧ length(b,bn);
⇔
  // sample solution: 6 lines using only the quantifiers ∀ and ∃
  ⊥ 
;

// compute the lexicographic relationship between 
// word a of length an and word b of length bn
proc compare(a:Word, an:Index, b:Word, bn:Index): Decision
  requires length(a,an) ∧ length(b,bn);
  ensures compares(a,an,b,bn,result);
{
  var i:Index = 0;
  while i < an ∧ i < bn ∧ a[i] = b[i] do
    i ≔ i+1;
  var d:Decision = 0;
  if i < an ∨ i < bn then
  {
    if i = an then
      d ≔ -1;
    else if i = bn then
      d ≔ 1;
    else if a[i] < b[i] then
      d ≔ -1;
    else
      d ≔ 1;
  }
  return d;
}

// -----------------------------------------------------------------
// end of file
// -----------------------------------------------------------------