// Programare Orientata Obiect in Dafny
class Cell
{
  var len : int        // as avea nevoie sa spun: len este "tot timpul" >= 0
    
  // invariant de clasa: o proprietate care are loc dupa apelul oricarei metode din clasa (si inainte)

  // nu exista o constructie speciala pentru a defini invarianti de clasa
  // dar exista o metodologie pentru definirea/folosirea lor

  ghost predicate Valid() // indeplineste invariantul de clasa
    reads this // ce referinte de pe heap acceseaza
    // din motive de eficienta a verificarii:
    // daca o metoda schimba cateva referinte pe heap, functiile/predicatele
    // care nu acceseaza acea zona nu isi schimba valoarea
  {
    len >= 0
  }

  constructor(initialValue : int)
    requires initialValue >= 0
    ensures len == initialValue
    ensures Valid()
  {
    this.len := initialValue;
  }

  constructor fromNothing()
    ensures len == 0
    ensures Valid()
  {
    this.len := 0;
  }

  constructor fromString(s : string)
    ensures len == |s|
    ensures Valid()
  {
    this.len := |s|;
  }

  method getLen() returns (r : int)
    requires Valid()
    ensures r == this.len
    ensures Valid()
  {
    return len;
  }

  method setLen(value : int)
    requires value >= 0
    // cadru de memorie pe care il poate modifica ("modifies" frame)
    // toate referintele la locatii din heap pe care risca sa le modifice
    // daca verificatorul stie ca o expresie nu foloseste
    //      partea din heap care risca sa se modifice
    // atunci valoarea expresiei nu se modifica dupa apelul metodei
    modifies this
    ensures this.len == value
    ensures Valid()
    // sau, daca vreau sa fiu mai explicit: modifies this`len
  {
    len := value;
  }

  method incrementLen()
    requires Valid()
    modifies this
    ensures len == old(len) + 1
    ensures Valid()
  {
    len := len + 1;
  }

  method decrementLen()
    requires Valid() // redundant
    requires len > 0
    modifies this
    ensures len == old(len) - 1
    ensures Valid()
  {
    len := len - 1;
  }
}

method Main()
{
  var cell := new Cell.fromNothing();
  print cell.len;
  print "\n";
  var len := cell.getLen();
  print len;
  print "\n";
  var cell1 := new Cell(0);
  cell1.setLen(7); // demonstreaza 7: int; nu se uita la continutul metodei;
  // adauga in context postconditiile
  cell1.decrementLen();
  assert cell1.len == 6;
  cell1.decrementLen();
  assert cell1.len == 5;
  print cell1.len, "\n";
  // doesn't work anymore: var cell2 := new Cell(-10);
  // doesn't work anymore: print "Lungimea este: ", cell2.len, "\n";

  var list1 := new Node.singleton(7);
  var list2 := new Node.pushFront(13, list1);
  var list3 := new Node.pushFront(42, list2);
  var x := list3.sum();
  print "Suma este: ", x, "\n";
}

method update(cells : seq<Cell>)
  requires |cells| > 2
  requires forall i, j :: 0 <= i < j < |cells| ==> cells[i] != cells[j]
  requires forall i :: 0 <= i < |cells| ==> cells[i].Valid()
  modifies cells // cells este o secventa de referinte
                 // modifica, potential, orice referinta din secventa
  ensures forall i :: 0 <= i < |cells| ==> cells[i].Valid()
{
  // cells := []; // secventa cells nu se poate schimba, este imuabila
  // ce pot schimba: obiectele din cells
  cells[0].incrementLen();
  cells[0].setLen(7);
  assert cells[0].len == 7;
  cells[1].setLen(13); // modifies cells[1]
                       // aliasing: mai multe valori care pointeaza spre aceeasi zona de memorie
  assert cells[0].len == 7; // acum poate demonstra, deoarece cells[0] != cells[1] (din al doilea requires)
  assert cells[1].len == 13;
 }

class Rational
{
  var n : int
  var m : int

  ghost predicate Valid()
    reads this
  {
    m != 0
  }

  constructor(n : int, m : int)
    requires m != 0
    ensures Valid()
    ensures this.n == n && this.m == m
  {
    this.n := n;
    this.m := m;
  }

  constructor fromInt(x : int)
    ensures Valid()
    ensures this.n == x && this.m == 1
  {
    this.n := x;
    this.m := 1;
  }

  ghost function value() : real
    requires Valid()
    reads this
  {
    (n as real) / (m as real)
  }

  method add(other : Rational)
    requires Valid()
    requires other.Valid()
    modifies this
    ensures Valid()
    ensures this.value() == old(this.value()) + other.value()
  {
    // this.n / this.m + other.n / other.m
    // this.n * other.m / this.m * other.m + other.n * this.m / other.m * this.m
    this.n := this.n * other.m + other.n * this.m;
    this.m := this.m * other.m;
    calc {
      this.value();
        ==
        {
          assume {:axiom} false;
        }
        old(this.value()) + other.value();
    }
  }
}

class MyNode
{
  var value : int
}

method ex1(head : MyNode)
{
  //assert head != null;
}

method ex2(head : MyNode?) // MyNode? este o referinta spre un MyNode sau null
  requires head != null
{
  assert head != null;
}

/*
method ex3(head : MyNode)
  requires head != null
{
  assert head != null;
}
 */

// lista inlantuita in still POO

function sumSeq(s : seq<int>) : int
{
  if |s| == 0 then
    0
  else
    s[0] + sumSeq(s[1..])
}

function sumSeq'(s : seq<int>) : int
{
  if |s| == 0 then
    0
  else
    s[|s| - 1] + sumSeq'(s[..|s| - 1])
}

lemma sumSeq_eq_sumSeq'(s : seq<int>)
  ensures sumSeq(s) == sumSeq'(s)
{
  assume {:axiom} false;
}

class Node
{
  var value : int
  var next : Node?

  ghost var repr : set<Node> // toate nodurile accesibile din nodul curent
                             // repr sau footprint
  ghost var values : seq<int> // toate valorile din lista
                             
  /*
     100: 7, 200         (repr = { 100, 200, 150 } )  // [ 7, 13, 42]
     150: 42, null       (repr = { 150 } )            // [ 42 ]
     200: 13, 150        (repr = { 200, 150 } )       // [ 13, 42 ]
   */
  ghost predicate Valid()
    // intr-adevar this este o lista simplu inlantuita (de exemplu, nu o lista circulara)
    reads this
    reads repr
    decreases repr
  {
    (next == null ==> (repr == { this } && values == [ value ])) &&
      (next != null ==>
      (
      this in repr &&
      this.next in repr &&
      this.next.repr <= this.repr &&
      this !in this.next.repr &&
      |this.values| > 0 && 
      this.values[0] == value &&
      this.next.values == this.values[1..] && 
      this.next.Valid()
      ))
  }

  constructor singleton(value : int)
    ensures this.value == value
    ensures this.next == null
    ensures Valid()
  {
    this.value := value;
    this.next := null;
    this.repr := { this };
    this.values := [ value ];
  }

  constructor pushFront(x : int, head : Node)
    requires head.Valid()
    ensures this.Valid()
  {
    this.value := x;
    this.next := head;
    this.repr := { this } + head.repr;
    this.values := [ x ] + head.values;
  }

  method sum() returns (r : int)
    requires Valid()
    ensures r == sumSeq(values)
  {
    var temp : int := 0;
    var curr : Node? := this;
    while curr != null
      invariant curr != null ==> curr.Valid()
      invariant curr != null ==> sumSeq(this.values) == temp + sumSeq(curr.values)
      invariant curr == null ==> sumSeq(this.values) == temp
      decreases if curr == null then {} else curr.repr
    {
      temp := temp + curr.value;
      curr := curr.next;
    }
    return temp;
  }
}

method loop()
{
  var n1 := new Node.singleton(7);
  var n2 := new Node.singleton(13);
  n1.next := n2;
  n2.next := n1;
  //var x := n1.sum();
}


method add10(head : Node) returns (r : Node)
  requires head.Valid()
  // ensures  suma noua = suma veche + 10
{
  r := new Node.pushFront(10, head);
}

trait Printable
{
  method Print()
}

class Cell' extends Printable, Stringable
{
  var contents : int
  constructor(x : int)
  {
    contents := x;
  }
  method Print()
  {
    print "I am a cell\n";
  }
  method toString(prefix : string) returns (r : string)
    requires true // preconditia: este mai slaba
    ensures |r| > 2 // postconditia: este mai puternica
    ensures prefix <= r
  {
    return prefix + "I am a cell";
  }
}

trait Stringable
{
  method toString(prefix : string) returns (r : string)
    requires |prefix| > 0
    ensures |r| > 0
    ensures prefix <= r
}

method useStringable()
{
  var c : Cell' := new Cell'(13);
  var x : Stringable := c;
  var p : Printable := c;
  var s := x.toString("asdf");
  // x.Print();
  p.Print();
  // cannot prove: assert s == "asdf" + "I am a cell";
  assert |s| > 0;
  assert "asdf" <= s;
}