/*@ <webex id="program" type="riscal"
       header="A Programming 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">@*/2/*@</input>@*/;
type int = ℕ[N];
type elem = ℕ[M];
type array = Array[N,elem];
/*@ <display>
Write 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. Formally, the procedure must satisfy the
following specification represented by precondition pre(a,na,b,nb) and
postcondition post(a,na,b,nb,c):
</display> @*/
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) 
  requires na+nb < N;
⇔ 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]));
/*@ <display>
Give here the body of merge(a,na,b,nb):
</display>
@*/
proc merge(a:array, na:int, b:array, nb:int): array
//@ <private>
  requires pre(a,na,b,nb);
  ensures post(a,na,b,nb,result);
//@ <public>
{
  //@ <input id="body" cols="70" rows="16">
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;//@ </input>


}
//@ <private>
//@<display>Check your implementation with respect to the specification:</display>
/*@ <button id="run" label="Check merge(a,na,b,nb)" action="merge">
    <argument value="-opt-si"> <argument option="silent">
</button>
@*/
//@<display></display>
//@ <option id="silent" label="Silent Execution:" type="bool">