A Specification Exercise

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];

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):

First investigate your specification:

Now further validate your specification:

Now check whether post() define the first na+nb elements of the result array
uniquely (the remaining elements are not of interest):

Finally check whether your specification specifies merge(a,na,b,nb) adequately: