/*@ <webex id="firstOrderPragmatics" type="riscal"
       header="Exercise: First Order Pragmatics" 
       href="http://fmv.jku.at/logik/index.html">
@*/

/*@ <display>
TASK DESCRIPTION: 

In the following we consider arrays of maximum length N whose elements are
natural numbers of maximum size M: 
</display> @*/

//@ <public>
val N = /*@<input id="N" cols="2">@*/4/*@</input>@*/; // choose small values
val M = /*@<input id="M" cols="2">@*/3/*@</input>@*/;
type Elem = ℕ[M];
type Arr = Array[N,Elem];
type Index = ℤ[-1,N];
//@ <private>

/*@ <display>
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.
</display> @*/

//@ <public>
pred P(a:Arr,n:Index,e:Elem) ⇔ 
//@ <input id="P" cols="70" rows="3">
  // formulate here the input condition
  0 ≤ n ∧ 
  ∃i:Index. 0 ≤ i ∧ i < n ∧ a[i] = e
//@ </input>
;

pred Q(a:Arr,n:Index,e:Elem,i:Index) ⇔ 
//@ <input id="Q" cols="70" rows="3">
  // formulate here the output condition
  0 ≤ i ∧ i < n ∧ a[i] = e ∧ 
  ∀i0:Index. 0 ≤ i0 ∧ i0 < n ∧ a[i0] = e ⇒ i ≤ i0
//@ </input>
;

/*@ <display>

TASK a: investigate the inputs/outputs allowed by your specification
(see for which inputs it allows which outputs):
</display> @*/
//@ <public>
fun compute(a:Arr,n:Index,e:Elem):Index 
  requires P(a,n,e); 
= choose i:Index with Q(a,n,e,i);
//@ <private>

/*@ <button id="compute" label="Run compute()" 
      action="compute">
      <argument value="-opt-si"> <argument value="0">
      <argument value="-opt-nd"> <argument value="1">
</button>@*/

/*@ <display>

TASKS b and c: check whether your input condition is satisfiable but not trivial.
</display> @*/

//@ <public>
theorem satP()     ⇔ ∃a:Arr,n:Index,e:Elem. P(a,n,e);
theorem nontrivP() ⇔ ∃a:Arr,n:Index,e:Elem. ¬P(a,n,e);
//@ <private>

/*@ <button id="satP" label="Check satP()" 
      action="satP">
      <argument value="-opt-si"> <argument value="0">
</button>@*/

//@ <display></display>

/*@ <button id="nontrivP" label="Check nontrivP()" 
      action="nontrivP">
      <argument value="-opt-si"> <argument value="0">
</button>@*/

/*@ <display>

TASKS d and e: check whether your output condition is satisfiable but not trivial.
</display> @*/

//@ <public>
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);
//@ <private>

/*@ <button id="satQ" label="Check satQ()" 
      action="satP">
      <argument value="-opt-si"> <argument value="0">
</button>@*/

//@ <display></display>

/*@ <button id="nontrivQ" label="Check nontrivQ()" 
      action="nontrivP">
      <argument value="-opt-si"> <argument value="0">
</button>@*/

/*@ <display>

TASK f: check whether your output condition defines the result uniquely:
</display> @*/

//@ <public>
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;
//@ <private>

/*@ <button id="uniqueQ" label="Check uniqueQ()" 
      action="uniqueQ">
      <argument value="-opt-si"> <argument value="0">
</button>@*/

/*@ <display>

TASK g: check whether your specification adequately specifies the following
code (is not too strong nor too weak):
</display> @*/

//@ <public>
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;
}
//@ <private>

//@ <display></display>

//@ <public>
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);
//@ <private>

/*@ <button id="correct" label="Check correct()" 
      action="correct">
      <argument value="-opt-si"> <argument value="0">
</button>@*/

//@ <public>
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);
//@ <private>

/*@ <button id="complete" label="Check complete()" 
      action="complete">
      <argument value="-opt-si"> <argument value="0">
</button>@*/