Exercise: First Order Pragmatics

TASK DESCRIPTION: 

In the following we consider arrays of maximum length N whose elements are
natural numbers of maximum size M: 

val N = 

; // choose small values
val M = 

;
type Elem = ℕ[M];
type Arr = Array[N,Elem];
type Index = ℤ[-1,N];

Take the problem of finding the smallest index i at which an element e occurs
among the first n elements of an array a:

    Input:  a ∈ Arr, n ∈ Index, e ∈ Elem where 

    - n is greater equal 0 and
    - e occurs among the first n elements in a, i.e.: 
          there exists some index i greater equal 0 but 
          less than n at which a holds e.

    Output: i ∈ Index where i is the smallest index at which e occurs among the 
    first n elements of a, i.e.:

    - i is greater equal 0 but less than n and a holds e at i 
    - i is less than equal all indices i0 that have the same property

The task is to develop a formal specification of this problem, i.e., to define a
predicate P(a,n,e), the input condition of the problem, and a predicate Q(a,n,e,i),
the output condition.

pred P(a:Arr,n:Index,e:Elem) ⇔ 

;

pred Q(a:Arr,n:Index,e:Elem,i:Index) ⇔ 

;

TASK a: investigate the inputs/outputs allowed by your specification
(see for which inputs it allows which outputs):

fun compute(a:Arr,n:Index,e:Elem):Index 
  requires P(a,n,e); 
= choose i:Index with Q(a,n,e,i);

TASKS b and c: check whether your input condition is satisfiable but not trivial.

theorem satP()     ⇔ ∃a:Arr,n:Index,e:Elem. P(a,n,e);
theorem nontrivP() ⇔ ∃a:Arr,n:Index,e:Elem. ¬P(a,n,e);

TASKS d and e: check whether your output condition is satisfiable but not trivial.

pred satQ()     ⇔ ∀a:Arr,n:Index,e:Elem. 
                    P(a,n,e) ⇒ ∃i:Index. Q(a,n,e,i);
pred nontrivQ() ⇔ ∃a:Arr,n:Index,e:Elem. 
                    P(a,n,e) ∧ ∃i:Index. ¬Q(a,n,e,i);

TASK f: check whether your output condition defines the result uniquely:

pred uniqueQ() ⇔ 
  ∀a:Arr,n:Index,e:Elem. P(a,n,e) ⇒ 
    ∀i1:Index,i2:Index. Q(a,n,e,i1) ∧ Q(a,n,e,i2) ⇒ i1 = i2;

TASK g: check whether your specification adequately specifies the following
code (is not too strong nor too weak):

proc search(a:Arr,n:Elem,e:Elem):Index
  requires P(a, n, e);
  ensures Q(a, n, e, result);
{
  var i:Index ≔ 0;
  var result:Index ≔ -1;
  while i < n ∧ result = -1 do
  {
    if a[i] = e then result ≔ i;
    i ≔ i+1;
  }
  return result;
}

theorem correct(a:Arr,n:Elem,e:Elem) 
  requires P(a,n,e);
⇔ let i = search(a,n,e) in Q(a,n,e,i);

theorem complete(a:Arr,n:Elem,e:Elem) 
  requires P(a,n,e);
⇔ ∀i:Index. Q(a,n,e,i) ⇒ i = search(a,n,e);