// Background theory starts here

// ----------------------------------------------------------------------
// Heap and allocation

// Function which defines a heap
function IsHeap(heap:[ref,<x>name]x) returns (bool);

// The global heap (which is always a heap)
var Heap: [ref, <x>name]x where IsHeap(Heap);

// Allocation field
const unique $allocated: <bool>name;

// Function to check if an object is allocated
function IsAllocated(heap: [ref, <x>name]x, o: any) returns (bool);
axiom (forall heap: [ref, <x>name]x, o: ref ::
            { IsAllocated(heap, o) } // Trigger
        IsAllocated(heap, o) <==> heap[o, $allocated]);

// Function to check if an object is allocated and not void
function IsAllocatedAndNotVoid(heap: [ref, <x>name]x, o: ref) returns (bool);
axiom (forall heap: [ref, <x>name]x, o: ref ::
            { IsAllocatedAndNotVoid(heap, o) } // Trigger
        IsHeap(heap) ==> (IsAllocatedAndNotVoid(heap, o) <==> o != null && heap[o, $allocated]));

// Function to check if an object is allocated if it is not void
function IsAllocatedIfNotVoid(heap: [ref, <x>name]x, o: ref) returns (bool);
axiom (forall heap: [ref, <x>name]x, o: ref ::
            { IsAllocatedIfNotVoid(heap, o) } // Trigger
        IsHeap(heap) ==> (IsAllocatedIfNotVoid(heap, o) <==> (o != null ==> heap[o, $allocated])));

// Every reference stored in the heap is allocated
// TODO: is this necessary?
//axiom (forall heap: [ref, <x>name]x, o: ref, f: <ref>name ::
//            { IsAllocated(heap, heap[o, f]) } // Trigger
//        IsHeap(heap) ==> IsAllocated(heap, heap[o, f]));

// Void are always allocated
axiom (forall heap: [ref, <x>name]x :: 
            { IsAllocated(heap, null) } // Trigger
        IsHeap(heap) ==> IsAllocated(heap, null));

// ----------------------------------------------------------------------
// Typing

// TODO: what functions do we need for typing?
function DeclaredType(field: name) returns (class: name);

// ----------------------------------------------------------------------
// Set theory

// ADT set
type set;

// Constructors
const set.make_empty: set;
function set.extended (set,any) returns (set);

// Content
function set.is_member (set,any) returns (bool);
axiom (forall s:set,x:any :: {set.is_member(set.extended(s,x),x)}
  set.is_member(set.extended(s,x),x));
axiom (forall s:set,x:any,y:any :: 
  x != y ==> set.is_member(set.extended(s,y),x) == set.is_member(s,x));
axiom (forall x:any :: !set.is_member (set.make_empty,x));

// Pruning
function set.pruned (set,any) returns (set);
axiom (forall x:any :: {set.pruned(set.make_empty,x)}
  set.pruned(set.make_empty,x) == set.make_empty);
axiom (forall s:set,x:any :: {set.pruned(set.extended(s,x),x)}
  set.pruned(set.extended(s,x),x) == set.pruned(s,x));
axiom (forall s:set,x:any,y:set :: {set.pruned(set.extended(s,x),y)}
  (x != y) ==> set.pruned(set.extended(s,x),y) == set.extended(set.pruned(s,y),x));

// Emptiness
function set.is_empty (set) returns (bool);
axiom (forall s:set,x:any :: !set.is_empty(set.extended(s,x)));
axiom (set.is_empty (set.make_empty));

// Cardinality
function set.cardinality (set) returns (int);
axiom (set.cardinality(set.make_empty) == 0);
axiom (forall s:set,x:any :: { set.cardinality(set.extended(s,x)) }
  !set.is_member(s,x) ==> 
    set.cardinality(set.extended(s,x)) == set.cardinality(s) + 1);
axiom (forall s:set,x:any :: { set.cardinality(set.extended(s,x)) }
  set.is_member(s,x) ==> 
    set.cardinality(set.extended(s,x)) == set.cardinality(s));

// Any element
function set.any_element (set) returns (any);
axiom (forall s:set,x:any :: set.any_element(set.extended(s,x)) == x);	

// Subset
function set.is_subset_of (set, set) returns (bool);
axiom (forall s:set :: set.is_subset_of (s, set.make_empty));
axiom (forall s1:set, s2:set, x:any :: 
  set.is_subset_of (s1, set.extended(s2, x)) == (set.is_subset_of (s1, s2) &&
    set.is_member (s1, x)));
	
// Equality
function set.equals (set, set) returns (bool);
axiom (forall s1:set, s2:set :: (s1 == s2) == (set.is_subset_of (s1, s2) &&
  set.is_subset_of (s2, s1)));
axiom (forall s1:set, s2:set :: (s1 == s2) == (set.equals (s1, s2)));

// Union
function set.united (set,set) returns (set);
axiom (forall s:set :: {set.united (s,set.make_empty)}
  set.united (s,set.make_empty) == s);
axiom (forall s1:set,s2:set,x:any :: {set.united(s1,set.extended(s2,x))}
  set.united(s1,set.extended(s2,x)) == set.extended(set.united(s1,s2),x));

// Intersected
function set.intersected (set,set) returns (set);
axiom (forall s:set :: {set.intersected(s,set.make_empty)}
  set.intersected(s,set.make_empty) == set.make_empty);
axiom (forall s1:set,s2:set,x:any :: {set.intersected(s1, set.extended(s2, x))}
  set.is_member(s1,x) ==> (set.intersected(s1,set.extended(s2,x))  == 
    set.extended (set.intersected(s1,s2),x)));
axiom (forall s1:set,s2:set,x:any :: {set.intersected(s1, set.extended(s2, x))}
  !set.is_member(s1,x) ==> (set.intersected(s1,set.extended(s2,x))  == 
    set.intersected(s1,s2)));
  
// Disjoint
function set.is_disjoint_from (set,set) returns (bool);
axiom (forall s:set :: {set.is_disjoint_from (s,set.make_empty)}
  set.is_disjoint_from (s,set.make_empty));
axiom (forall s1:set,s2:set,x:any :: set.is_disjoint_from (s1,set.extended(s2,x)) ==
  (!set.is_member(s1,x) && set.is_disjoint_from (s1, s2)));
axiom (forall s1:set, s2:set :: set.is_disjoint_from (s1, s2) == set.is_disjoint_from (s2, s1));

// Superset
function set.is_superset_of (set, set) returns (bool);
axiom (forall s1:set, s2:set :: {set.is_superset_of (s1, s2)}
	set.is_superset_of (s1, s2) == set.is_subset_of (s2, s1));
	
// proper Subset
function set.is_proper_superset (set, set) returns (bool);
axiom (forall s1:set, s2:set :: {set.is_proper_superset (s1, s2)}
  set.is_proper_superset (s1, s2) == (set.is_subset_of (s2, s1) && (s1 != s2)));

// proper Superset
function set.is_proper_subset (set,set) returns (bool);
axiom (forall s1:set,s2:set :: {set.is_proper_subset (s1, s2)}
  set.is_proper_subset (s1,s2) == (set.is_subset_of (s1, s2) && (s1 != s2)));

// Substracted
function set.subtracted (set,set) returns (set);
axiom (forall s:set :: {set.subtracted(s,set.make_empty)}
  set.subtracted(s,set.make_empty) == s);
axiom (forall s1:set,s2:set,x:any :: {set.subtracted(s1,set.extended(s2,x))}
  set.subtracted(s1,set.extended(s2,x)) == set.pruned(set.subtracted(s1,s2),x));

// Difference
function set.difference (set,set) returns (set);
axiom (forall s1:set,s2:set :: {set.difference(s1,s2)}
  set.difference(s1,s2) == set.subtracted(set.united(s1,s2),set.intersected(s1,s2)));

// ----------------------------------------------------------------------
// Agent theory

// Precondition functions for different number of arguments

function routine.precondition_0 (heap: [ref,<x>name]x, agent: ref) returns (bool);
function routine.precondition_1 (heap: [ref,<x>name]x, agent: ref, arg1: any) returns (bool);
function routine.precondition_2 (heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any) returns (bool);
function routine.precondition_3 (heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any) returns (bool);
function routine.precondition_4 (heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any, arg4: any) returns (bool);
function routine.precondition_5 (heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any, arg4: any, arg5: any) returns (bool);

// Postcondition functions for different number of arguments

function routine.postcondition_0 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref) returns (bool);
function routine.postcondition_1 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any) returns (bool);
function routine.postcondition_2 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any) returns (bool);
function routine.postcondition_3 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any) returns (bool);
function routine.postcondition_4 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any, arg4: any) returns (bool);
function routine.postcondition_5 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any, arg4: any, arg5: any) returns (bool);

// Postcondition functions for different number of arguments and return values

function function.postcondition_0 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, result: any) returns (bool);
function function.postcondition_1 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, result: any) returns (bool);
function function.postcondition_2 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, result: any) returns (bool);
function function.postcondition_3 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any, result: any) returns (bool);
function function.postcondition_4 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any, arg4: any, result: any) returns (bool);
function function.postcondition_5 (heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref, arg1: any, arg2: any, arg3: any, arg4: any, arg5: any, result: any) returns (bool);

// Frame condition function

function agent.modifies(agent: ref, $o: ref, $f: name) returns (bool);

// Agent creation

procedure routine.create(
        Current: ref where Current != null && !Heap[Current,$allocated]    // The agent object
    );
    modifies Heap;
    // Frame condition
    ensures frame.modifies_current (Heap, old(Heap), Current);
    // Object allocated
    free ensures Heap[Current, $allocated];

// Call functions for different number of arguments

procedure routine.call_0 (
        Current: ref where Current != null && Heap[Current,$allocated]     // The agent object
    );
    requires routine.precondition_0(Heap, Current); // pre ROUTINE:call tag:precondition
    modifies Heap;
    ensures (forall $o: ref, $f: name :: { Heap[$o, $f] } ($o != null && old(Heap)[$o, $allocated] && !agent.modifies(Current, $o, $f)) ==> (old(Heap)[$o, $f] == Heap[$o, $f])); // frame ROUTINE:call
    ensures routine.postcondition_0(Heap, old(Heap), Current);

procedure routine.call_1 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any                                                           // First argument
    );
    requires routine.precondition_1(Heap, Current, arg1); // pre ROUTINE:call tag:precondition
    modifies Heap;
    ensures (forall $o: ref, $f: name :: { Heap[$o, $f] } ($o != null && old(Heap)[$o, $allocated] && !agent.modifies(Current, $o, $f)) ==> (old(Heap)[$o, $f] == Heap[$o, $f])); // frame ROUTINE:call
    ensures routine.postcondition_1(Heap, old(Heap), Current, arg1);

procedure routine.call_2 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any                                                           // Second argument
    );
    requires routine.precondition_2(Heap, Current, arg1, arg2); // pre ROUTINE:call tag:precondition
    modifies Heap;
    ensures (forall $o: ref, $f: name :: { Heap[$o, $f] } ($o != null && old(Heap)[$o, $allocated] && !agent.modifies(Current, $o, $f)) ==> (old(Heap)[$o, $f] == Heap[$o, $f])); // frame ROUTINE:call
    ensures routine.postcondition_2(Heap, old(Heap), Current, arg1, arg2);

procedure routine.call_3 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any,                                                          // Second argument
        arg3: any                                                           // Third argument
    );
    requires routine.precondition_3(Heap, Current, arg1, arg2, arg3); // pre ROUTINE:call tag:precondition
    modifies Heap;
    ensures (forall $o: ref, $f: name :: { Heap[$o, $f] } ($o != null && old(Heap)[$o, $allocated] && !agent.modifies(Current, $o, $f)) ==> (old(Heap)[$o, $f] == Heap[$o, $f])); // frame ROUTINE:call
    ensures routine.postcondition_3(Heap, old(Heap), Current, arg1, arg2, arg3);

procedure routine.call_4 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any,                                                          // Second argument
        arg3: any,                                                          // Third argument
        arg4: any                                                           // Fourth argument
    );
    requires routine.precondition_4(Heap, Current, arg1, arg2, arg3, arg4); // pre ROUTINE:call tag:precondition
    modifies Heap;
    ensures (forall $o: ref, $f: name :: { Heap[$o, $f] } ($o != null && old(Heap)[$o, $allocated] && !agent.modifies(Current, $o, $f)) ==> (old(Heap)[$o, $f] == Heap[$o, $f])); // frame ROUTINE:call
    ensures routine.postcondition_4(Heap, old(Heap), Current, arg1, arg2, arg3, arg4);

procedure routine.call_5 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any,                                                          // Second argument
        arg3: any,                                                          // Third argument
        arg4: any,                                                          // Fourth argument
        arg5: any                                                           // Fifth argument
    );
    requires routine.precondition_5(Heap, Current, arg1, arg2, arg3, arg4, arg5); // pre ROUTINE:call tag:precondition
    modifies Heap;
    ensures (forall $o: ref, $f: name :: { Heap[$o, $f] } ($o != null && old(Heap)[$o, $allocated] && !agent.modifies(Current, $o, $f)) ==> (old(Heap)[$o, $f] == Heap[$o, $f])); // frame ROUTINE:call
    ensures routine.postcondition_5(Heap, old(Heap), Current, arg1, arg2, arg3, arg4, arg5);

// Item functions for different number of arguments

procedure function.item_0 (
        Current: ref where Current != null && Heap[Current,$allocated]     // The agent object
    ) returns (Result: any);
    requires routine.precondition_0(Heap, Current);
    modifies Heap;
    ensures frame.modifies_agent(Heap, old(Heap), Current); // frame FUNCTION:item
    ensures function.postcondition_0(Heap, old(Heap), Current, Result);

procedure function.item_1 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any                                                           // First argument
    ) returns (Result: any);
    requires routine.precondition_1(Heap, Current, arg1);
    modifies Heap;
    ensures frame.modifies_agent(Heap, old(Heap), Current); // frame FUNCTION:item
    ensures function.postcondition_1(Heap, old(Heap), Current, arg1, Result);

procedure function.item_2 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any                                                           // Second argument
    ) returns (Result: any);
    requires routine.precondition_2(Heap, Current, arg1, arg2);
    modifies Heap;
    ensures frame.modifies_agent(Heap, old(Heap), Current); // frame FUNCTION:item
    ensures function.postcondition_2(Heap, old(Heap), Current, arg1, arg2, Result);

procedure function.item_3 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any,                                                          // Second argument
        arg3: any                                                           // Third argument
    ) returns (Result: any);
    requires routine.precondition_3(Heap, Current, arg1, arg2, arg3);
    modifies Heap;
    ensures frame.modifies_agent(Heap, old(Heap), Current); // frame FUNCTION:item
    ensures function.postcondition_3(Heap, old(Heap), Current, arg1, arg2, arg3, Result);

procedure function.item_4 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any,                                                          // Second argument
        arg3: any,                                                          // Third argument
        arg4: any                                                           // Fourth argument
    ) returns (Result: any);
    requires routine.precondition_4(Heap, Current, arg1, arg2, arg3, arg4);
    modifies Heap;
    ensures frame.modifies_agent(Heap, old(Heap), Current); // frame FUNCTION:item
    ensures function.postcondition_4(Heap, old(Heap), Current, arg1, arg2, arg3, arg4, Result);

procedure function.item_5 (
        Current: ref where Current != null && Heap[Current,$allocated],     // The agent object
        arg1: any,                                                          // First argument
        arg2: any,                                                          // Second argument
        arg3: any,                                                          // Third argument
        arg4: any,                                                          // Fourth argument
        arg5: any                                                           // Fifth argument
    ) returns (Result: any);
    requires routine.precondition_5(Heap, Current, arg1, arg2, arg3, arg4, arg5);
    modifies Heap;
    ensures frame.modifies_agent(Heap, old(Heap), Current); // frame FUNCTION:item
    ensures function.postcondition_5(Heap, old(Heap), Current, arg1, arg2, arg3, arg4, arg5, Result);

// ----------------------------------------------------------------------
// Frame conditions

// Frame condition for a feature which modifies nothing.
function frame.modifies_nothing(heap: [ref,<x>name]x, old_heap: [ref,<x>name]x) returns (bool);
axiom (forall heap: [ref,<x>name]x, old_heap: [ref,<x>name]x :: 
            { frame.modifies_nothing(heap, old_heap) } // Trigger
        frame.modifies_nothing(heap, old_heap) <==> 
            (forall $o: ref, $f: name :: 
                    { heap[$o, $f] } // Trigger
                ($o != null && old_heap[$o, $allocated]) ==> (old_heap[$o, $f] == heap[$o, $f])));

// Frame condition for a feature which modifies only the `Current' object.
function frame.modifies_current(heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, current: ref) returns (bool);
axiom (forall heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, current: ref :: 
            { frame.modifies_current(heap, old_heap, current) } // Trigger
        frame.modifies_current(heap, old_heap, current) <==> 
            (forall $o: ref, $f: name :: 
                    { heap[$o, $f] } // Trigger
                ($o != null && old_heap[$o, $allocated] && $o != current) ==> (old_heap[$o, $f] == heap[$o, $f])));

// Frame condition for a feature which modifies what the `agent' modifies.
function frame.modifies_agent(heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref) returns (bool);
axiom (forall heap: [ref,<x>name]x, old_heap: [ref,<x>name]x, agent: ref :: 
            { frame.modifies_agent(heap, old_heap, agent) } // Trigger
        frame.modifies_agent(heap, old_heap, agent) <==> 
            (forall $o: ref, $f: name :: 
                    { heap[$o, $f] } // Trigger
                ($o != null && old_heap[$o, $allocated] && !agent.modifies(agent, $o, $f)) ==> (old_heap[$o, $f] == heap[$o, $f])));