// ghost function abs'(x : int) : int
// {
//   if x < 0 then
//     -x
//   else
//     x
// }

// method abs(x : int) returns (r : int)
//   ensures r == abs'(x)            // -> metoda 1
//   // ensures r >= 0                      // -> metoda 2
//   // ensures r == -x || r == x
// {
//   if (x < 0) {
//     r := -x;
//   } else {
//     r := x;
//   }
// }

// FUNCTION = METHOD + GHOST FUNCTION

function abs(x : int) : int
{
  if x < 0 then
    -x
  else
    x
}

ghost function perfectSquare(x : int) : bool
{
  exists y :: y * y == x
}

ghost predicate perfectSquare'(x : int)
{
  exists y :: y * y == x
}

// method Main()
// {
//   // var x := abs(-13);
//   // ghost var y := abs'(-13);
//   // print x;
//   // print y;
//   var x := abs(-13);
//   print x;
// }

// SECVENTE

function first(s : seq<int>) : int
  requires |s| > 0
{
  s[0]
}

function update(s : seq<int>, i : int, v : int) : seq<int>
  requires 0 <= i < |s|
{
  s[i := v]
}

method asdf(a : array<int>, i : int, v : int)
  requires 0 <= i < a.Length
  modifies a
{
  a[i] := v;
}

method mult2(a : array<int>)
  modifies a
  ensures forall i :: 0 <= i < a.Length ==> a[i] == old(a[i]) * 2
{
  var i := 0;
  while (i < a.Length)
    invariant 0 <= i <= a.Length
    invariant forall j :: 0 <= j < i ==> a[j] == old(a[j]) * 2
    //invariant forall j :: i <= j < a.Length ==> a[j] == old(a[j])
    invariant a[i..] == old(a[i..])
  {
    a[i] := a[i] * 2;
    i := i + 1;
  }
}



method Main()
{
  var s : seq<int> := [ 4, 3, 7, 9 ];
  var s' : seq<int> := update(s, 2, 10);
  // SLICE NOTATION
  var s'' := s[1..3];
  var s''' := s[1..];
  var s'''' := s[..3];
  var s''''' := s[..];
  var x := first(s);
  print x, "\n";
  print s', "\n";
  print s'', "\n";
  print s''', "\n";
  print s'''', "\n";
  print s''''', "\n";
  var s1 := [1, 2, 5, 7];
  var s2 := [1, 2];
  assert s2 < s1;
  assert s2 <= s1;
  assert s1 <= s1;
  // assert s1 < s1; // nu e prefix strict
  assert s1 + s2 == [ 1, 2, 5, 7, 1, 2 ];
  assert 5 in s1;
  assert 10 !in s1;
  var s3 := seq(10, i => i * i);
  print s3, "\n";
}