/* Copyright © 2010 The Crowfoot Team (Billiejoe Charlton, Ben Horsfall, Bernhard Reus) */


/* This is the initial webserver program, with no updates done. */


/* For modelling purposes, 'version' is a constant heap address where we store the version
   number of the system running currently. In this file, this will remain at 1. */

const version;


/* Modules */

const serverOne;
const handlersOne;

const serverLatest;
const handlersLatest;


/* Offsets for the various procedures in each module. */

/* Server module */

const getevent = 0;
const handle = 1;
const loop = 2;

/* Handlers module */

const handleGet = 0;
const handlePost = 1;
const handleUpdate = 2;


/* 'Abstract' (universally quantified) predicates for request data, and queues. */

forall $GetRequest(_).
forall $PostRequest(_).

forall $Queue(_,_).
forall $NonEmptyQueue(_,_).  /* Second argument is a counter for how many messages have been dequeued,
                                that can be reset with the reset() procedure (see later) */

/* Three different kinds of event can happen. */

const evGet = 0;
const evPost = 1;
const evUpdate = 2;

recdef $Event(e) :=

      e |-> evGet *  $GetRequest(e+1)
    | e |-> evPost * $PostRequest(e+1)
    | e |-> evUpdate;


/* The $CodeOne predicate describes the behaviour of the code for version 1 of webserver,
   once it is stored on the heap. */

recdef $CodeOne() :=

handlersOne+handleGet |->
forall q,req,n.
  { $GetRequest(req) * $Queue(q,n) }
  _(q,req)
  { $Queue(q,n) }

*

handlersOne+handlePost |->
forall q,req,n.
  { $PostRequest(req) * $Queue(q,n) }
  _(q,req)
  { $Queue(q,n) }

*
  
handlersOne+handleUpdate |->
forall ver.
  { $Code(1) }
  _()
  { $Code(1) }  

*

serverOne+getevent |->
forall q,n.
  { $Queue(q,n) }
  _(q)
  { $NonEmptyQueue(q,n) }

*

serverOne+handle |->
forall q,n.
  { $Code(1) * $NonEmptyQueue(q,n) }
  _(q)
  { $Code(1) * $Queue(q,n+1) }

*

serverOne+loop |->
forall q.  
  { exists n. $Code(1) * $Queue(q,n) }
  _(q)
  { false }
;



/* The $Code(v) predicate describes version v of the system (in this file, just version 1)
   with code stored on the heap, and the pointers to the latest versions. */ 

recdef $Code(v) :=

v = 1  * version |-> 1

*

$CodeOne()

  * handlersLatest |-> handlersOne
  * serverLatest |-> serverOne
;    


/* We leave handleGet and handlePost abstract, corresponding to the "..." in the
   "Formalizing Dynamic Software Updating" paper (Bierman, Hicks, Sewell, Stoyle). */

proc abstract handleGet(q,req)
  forall n.
  pre:  $GetRequest(req) * $Queue(q,n);
  post: $Queue(q,n);

proc abstract handlePost(q,req)
  forall n.
  pre:  $PostRequest(req) * $Queue(q,n);
  post: $Queue(q,n);


proc abstract getevent(q)
 forall n.
  pre:  $Queue(q,n);
  post: $NonEmptyQueue(q,n);

proc handleUpdate()
  pre:  $Code(1);
  post: $Code(1);
  
  {
  	call update()
  }


/* This procedure models the 'update' steps of the update calculus. In the initial program
   this does nothing. */

proc update()
  pre:  $Code(1);
  post: $Code(1);
  
  {
    skip  	
  }



proc handle(q)
 forall n.
  pre:  $Code(1) * $NonEmptyQueue(q,n);
  post: $Code(1) * $Queue(q,n+1);
  
  {
  	locals ePtr, event, eventType, req;
  	
  	ePtr := new 0;
  	call dequeue(q,ePtr);
  	event := [ePtr];
	dispose ePtr;
	
	ghost "unfold $Event(?)";
	
	eventType := [event];
	req := event+1;
	
	if eventType = evGet then
	  {
	  	eval [handlersOne+handleGet](q,req)
	  }
	else
	  {
	  	if eventType = evPost then
	  	  {
	  	  	eval [handlersOne+handlePost](q,req)
	  	  }
	  	else
	  	  {
	  	  	eval [handlersOne+handleUpdate]()
	  	  }
	  };
	 
  	dispose event 
  }


proc loop(q)

  pre:  exists n. $Code(1) * $Queue(q,n);
  post: false;

  {
    locals tmp;

    ghost "unfold $Code(1)";
    tmp := [serverLatest];
    ghost "fold $Code(1)";
    eval [tmp+getevent](q);

    ghost "unfold $Code(1)";
    tmp := [serverLatest];
    ghost "fold $Code(?)";
    eval [tmp+handle](q);

    ghost "unfold $Code(?)";
    tmp := [serverLatest];
    ghost "fold $Code(?)";
    eval [tmp+loop](q)
  }


proc main()

  pre:
      version |-> _
      
    /* Initial: */
    
    * handlersOne |-> 0,0,0  /* to hold procedures: handleGet,handlePost,handleUpdate */
    * serverOne |-> 0,0,0    /* to hold procedures: getevent, handle, loop */
    
	/* These will hold pointers to the latest versions */
	* handlersLatest |-> 0
	* serverLatest |-> 0;

  post: false; /* The program never terminates */
    
  {
    locals qPtr,q;
  	
  	[version] := 1;
  	
    /* We begin by writing all the procedures onto the heap. */

    [serverOne+getevent] := getevent(_);
    [serverOne+handle] := handle(_);
    [serverOne+loop] := loop(_);

    [handlersOne+handleGet] := handleGet(_,_);
    [handlersOne+handlePost] := handlePost(_,_);
    [handlersOne+handleUpdate] := handleUpdate();

	ghost "fold $CodeOne()";

    /* Then we set up the "latest" pointers to point to version 1. */

    [serverLatest] := serverOne;
    [handlersLatest] := handlersOne;
    
    ghost "fold $Code(1)";
  
    /* We create an empty queue, and then call 'loop' to start the server. */
  	
    qPtr := new 0;
    call mk_empty_queue(qPtr);
    q := [qPtr];
    dispose qPtr;

    eval [serverOne+loop](q)
  }




/* =========================
   Abstract queue operations
   ========================= */
    

proc abstract mk_empty_queue(qPtr)
  pre:  qPtr |-> _;
  post: exists q. qPtr |-> q * $Queue(q,0);


proc abstract dequeue(q,ePtr)
forall n.
  pre:  $NonEmptyQueue(q,n) * ePtr |-> _;
  post: exists e. $Queue(q,n+1) * ePtr |-> e * $Event(e);


proc abstract reset(q) /* This operation resets the internal dequeued messages counter */
pre:  exists n. $Queue(q,n);
post: $Queue(q,0);