/*@ <webex id="specification" type="riscal"
       header="A Specification Exercise" 
       href="https://www.risc.jku.at/research/formal/software/RISCAL">
@*/

/*@ <display>
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">@*/1/*@</input>@*/;
type int = ℕ[N];
type elem = ℕ[M];
type array = Array[N,elem];
/*@ <display>
Specify a procedure "merge(a,na,b,nb)" that takes two arrays a and b of size na
and nb, respectively, where na+nb is less than equal N and both a and b are
sorted in ascending order. The procedure returns an array c of size na+nb which
represents the "merged" version of a and b: c is also sorted in ascending order
and contains all elements of a and b. In detail, define the precondition
pre(a,na,b,nb) and postcondition post(a,na,b,nb,c) of the procedure (it is
recommended, to define an auxiliary predicate sorted(a,n) that states that array
a is sorted in the first n positions):
</display> @*/
//@ <input id="spec" cols="70" rows="16">
pred sorted(a:array, n:int) ⇔ 
  ∀i:int with 0 ≤ i ∧ i+1 < n. a[i] ≤ a[i+1]
;

pred pre(a:array, na:int, b:array, nb:int) ⇔
  na+nb < N ∧ sorted(a,na) ∧ sorted(b,nb)
;

pred post(a:array, na:int, b:array, nb:int, c:array) ⇔ 
  sorted(c,na+nb) ∧
  (∃p:Array[N,ℕ[N]].
    (∀i:int, j:int with i < j ∧ j < na+nb. p[i] ≠ p[j]) ∧
    (∀i:int with i < na+nb. 
       let j=p[i] in
       j < na+nb ∧ if j < na then c[i]=a[j] else c[i]=b[j-na]))
;
//@ </input>
//@ <private>
fun result(a:array, na:int, b:array, nb:int):array
  requires pre(a,na,b,nb);
= choose c:array with post(a,na,b,nb,c);

theorem satisfiable(a:array, na:int, b:array, nb:int) 
  requires pre(a,na,b,nb);
⇔ ∃c:array. post(a,na,b,nb,c);

theorem nottrivial() 
⇔ ∃a:array, na:int, b:array, nb:int with pre(a,na,b,nb).
    ∃c:array. ¬post(a,na,b,nb,c);

theorem unique(a:array, na:int, b:array, nb:int) 
  requires pre(a,na,b,nb);
⇔ ∀c1:array with post(a,na,b,nb,c1).
  ∀c2:array with post(a,na,b,nb,c2).
    ∀i:int with 0 ≤ i ∧ i < na+nb.
      c1[i] = c2[i];
   
//@<display>First investigate your specification:</display>
/*@ <button id="result" label="Show outputs allowed by post()" 
      action="result">
      <argument value="-opt-si"> <argument value="0">
      <argument value="-opt-nd"> <argument value="1">
</button>@*/

//@<display>Now further validate your specification:</display>
/*@ <button id="satisfiable" label="Is post() satisfiable?" 
      action="satisfiable">
      <argument value="-opt-si"> <argument value="1">
</button>
@*/

//@<display></display>
/*@ <button id="nottrivial" label="Is post() not trivial?" 
      action="nottrivial">
      <argument value="-opt-si"> <argument value="1">
</button>
@*/

/*@<display>
Now check whether post() define the first na+nb elements of the result array
uniquely (the remaining elements are not of interest):
</display>@*/

/*@ <button id="unique" label="Does post() uniquely define result?" 
      action="unique">
      <argument value="-opt-si"> <argument value="1">
      <argument value="-opt-mt"> <argument value="1">
      <argument value="-opt-tr"> <argument value="4">
</button>
@*/

proc merge(a:array, na:int, b:array, nb:int): array
{
var c:array = Array[N,elem](0);

var ia:int ≔ 0; var ib:int ≔ 0;       
for var i:int = 0; i<na+nb; i≔i+1 do
{
  if ia < na ∧ (ib = nb ∨ a[ia] ≤ b[ib]) then
  {
    c[i] ≔ a[ia]; ia ≔ ia+1;
  }
  else
  {
    c[i] ≔ b[ib]; ib ≔ ib+1;
  }
}

return c;
}

theorem notTooStrong(a:array, na:int, b:array, nb:int)
  requires pre(a,na,b,nb);
⇔ post(a, na, b, nb, merge(a, na, b, nb));

theorem notTooWeak(a:array, na:int, b:array, nb:int, c:array)
  requires pre(a,na,b,nb) ∧ post(a, na, b, nb, c);
⇔  let c0 = merge(a, na, b, nb) in
    ∀i:int with 0 ≤ i ∧ i < na+nb.
      c[i] = c0[i];

/*@<display>
Finally check whether your specification specifies merge(a,na,b,nb) adequately:
</display>@*/
/*@ 
<button id="notTooStrong" label="Is specification not too strong?" action="notTooStrong">
    <argument value="-opt-si"> <argument value="1">
</button>
@*/
//@<display></display>
/*@ 
<button id="notTooWeak" label="Is specification not too weak?" action="notTooWeak">
    <argument value="-opt-si"> <argument value="1">
    <argument value="-opt-mt"> <argument value="1">
    <argument value="-opt-tr"> <argument value="4">
</button>
@*/