#pragma CIVL ACSL

$input int N, M;
$assume(0 <= M && M < N);
$input int a[N];

int main() {
  int b[N];
  int old = b[M];
  /*@ loop invariant 0 <= i <= N;
    @ loop invariant \forall int i1; 0 <= i1 < i ==> 
    @                           ((i1 < M ==> b[i1] == 0) && (i1 > M ==> b[i1] == a[i1]));
    @ loop assigns i, b[0 .. M-1], b[M+1 .. N-1];
    @*/
  for (int i = 0; i < N; i++) {
    if (i < M) b[i] = 0;
    else if (i > M) b[i] = a[i];
  }
  //$assert($forall (int i : 0 .. N-1) (i < M ? b[i] == 0 : (i > M ? b[i] == a[i] : $true)));
  $assert($forall (int i : 0 .. N-1) (i < M => b[i] == 0) && (i > M => b[i] == a[i]));
  $assert(b[M] == old);
}