RISC JKU
JKU LIT Project LogTechEdu

A Programming Exercise


0 of 1 grade points have been earned so far.

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 int = ℕ[N];
type elem = ℕ[M];
type array = Array[N,elem];
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):
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]));
Give here the body of merge(a,na,b,nb):
proc merge(a:array, na:int, b:array, nb:int): array
{
  

}
Check your implementation with respect to the specification:

        
        
       

0 of 1 grade points have been earned so far.