// -----------------------------------------------------------------
// replacing values in an array
// -----------------------------------------------------------------

val N:ℕ; // length of array
val M:ℕ; // maximum size of array elements
val R:ℕ; // number of replacements
axiom notNull ⇔ N > 0 ∧ R > 0;

val I = if N > R then N else R; // maximum array length

type int = ℤ[-1,I]; // array indices (including -1 and I)
type value = ℕ[M];  // array elements

// the input condition
pred input(a:Array[N,value],from:Array[R,value],to:Array[R,value]) ⇔
  // sample solution: 1 line
  ⊤;

// the output condition
pred output(a:Array[N,value],from:Array[R,value],to:Array[R,value],b:Array[N,value]) ⇔
  // sample solution: 5 lines (involving ∀, ∃, if)
  ⊤;
      
// return duplicate of 'a' where every occurrence of an element
// in 'from' is replaced by the corresponding element in 'to'
// ('from' must not have duplicate elements)
proc replace(a:Array[N,value],from:Array[R,value],to:Array[R,value]):Array[N,value] 
  requires input(a,from,to);
  ensures output(a,from,to,result);
{
  var b:Array[N,value] ≔ Array[N,value](0);
  for var i:int ≔ 0; i < N; i ≔ i+1 do
  {
    var j:int ≔ 0;
    while j < R ∧ a[i] ≠ from[j] do j ≔ j+1;
    if j < R then b[i] = to[j]; else b[i] ≔ a[i];
  }
  return b;
}

// -----------------------------------------------------------------
// end of file
// -----------------------------------------------------------------