#include <vcc.h>

#define NULL 0



struct xLIST_ITEM;

struct xListMap;

_(ghost enum xListType {FIFO,PQ,UNORDERED} )

/*	Following variable represents the 
	maximum numeric value allowed by the type
*/
unsigned maxNumVal;
/*	Following variable represents the 
	maximum priority of a task
*/
ghost unsigned maxPrio;

_(dynamic_owns)
typedef struct tskTCB{
	struct xLIST_ITEM *pvGenericListItem;		
	/*  List item used to place the owner 
		task in ready or delayed/suspended lists. 
	*/
	struct xLIST_ITEM *pvEventListItem;		
	/*	List item used to place the owner task in 
		event lists. 
	*/
	unsigned uxPriority;			
	/*	The priority of the task where 0 is the 
		lowest priority. 
	*/

	_(invariant pvGenericListItem != pvEventListItem )
	/*	List items are distinct. */
}TCB;

_(dynamic_owns)
typedef struct xLIST_ITEM{
	unsigned xItemValue;	
	/* Can be the priority of the task or 
		time to awake in delayed lists
	*/
	struct xLIST_ITEM * pxNext;	
	/*	Pointer to the next xListItem in the list. */
	struct xLIST_ITEM * pxPrevious;
	/*  Pointer to the previous xListItem in the list.*/ 
	TCB * pvOwner;							
	/*	Pointer to the object (normally a TCB) 
		that owns the list item.  
	*/
	struct xListMap *pvContainer;   
	/*	pointer to the list in which it is present*/
	unsigned ownersPriority;	
	/* Extra field to represent the priority of the owner.
	   Without this, invariants on this field is not possible 
	   in the list because of ownership issue, note that at 
	   the same time two list items of a task can be 
	   in two different lists and hence neither can own the 
	   owner task 
	*/

} xListItem;



_(dynamic_owns)
typedef struct xListMap{

	/*	Following map models a sequence of nodes 
		(each node represent a task in the system), 
		the value for a given unsigned int 'i' gives 
		the address of the node modelling the ith 
		task in the sequence 
	*/
	_(ghost xListItem *list[unsigned] )
	/*	The following map support easy specification 
		of some of the function contract.
		The value of the following map for a given 
		pointer (p) to xListItem gives the index 
		(0<=index<length) of p in the list, 
		when p is present in list. If p is not in list, 
		the value should be 'length'. 
	*/
	_(ghost unsigned position[xListItem *] )
	/*	The following field shows the type (PQ or FIFO) 
		of the list. We need to specify properties 
		which are true only on lists of a given 'type'
	*/
	_(ghost enum xListType type )

	/*	The following field models the length of 
		the sequence 
	*/
	unsigned length;
	/*	Following ghost field models the priority 
		of tasks (unique) in ready queue. The value 
		is the priority of any task in this queue. 
		This enable easy specification.
	*/
	_(ghost unsigned priority )
	/*INV-1:	length never exceeds maxNumVal*/
	_(invariant length <= maxNumVal)
	/*INV-2:	priority of each task 
				is within the bound 
	*/
	_(invariant \forall unsigned i; ( i < length ) ==> 
			(	\mine(list[i])  && 
				( list[i]->ownersPriority <= maxPrio ) 
			)	
	 )
	/*INV-3:	item value of each node is within 
				the bound 
	*/
	_(invariant \forall unsigned i; 
		( (i<length) ==>
			(	\mine(list[i]) && 
				(list[i]->xItemValue<=maxNumVal) 
			)
		)
	 )
	/*INV-4:	Tasks in the list are distinct */
	_(invariant \forall unsigned i,j;
				(	(		(i<length) && (j<length) && (i!=j) && 
							\mine(list[i])  && \mine(list[j]) 
					) ==> ( list[i]->pvOwner != list[j]->pvOwner) 
				)
	 )

	/*INV-5:	Valid list elements are owned by this : 
				to support INV-2,INV-3 and INV-4
	*/
	_(invariant \forall unsigned i; ( i<length ) ==> 
				( (list[i] != NULL) && \mine(list[i]) ) 
	 )
	/*INV-6a:	position is consistent with list	*/
	_(invariant \forall xListItem *xli; \mine(xli) ==>	
			(	( position[xli]<length ) && 
				( list[position[xli]] == xli )
			)
	 )
	/*INV-6b:	position is consistent with list.
				Follows from the above. But explicitly 
				saying thhis helps the prover.
	*/
	_(invariant \forall unsigned i; (i<length) ==> 
			( \mine(list[i]) && (position[list[i]] == i) )
	 )
	/*INV-6c:	For all invalid list item modes, 
				value under the map position is 
				maxNumVal. 
	*/
	_(invariant \forall xListItem *xli; 
				( !\mine(xli) ) ==> ( position[xli]==maxNumVal ) 
	 ) 
	/*INV-7:	All invalid elements in the sequence 
				contain null pointer
	*/
	_(invariant \forall unsigned i; ( i>=length ) ==> 
									(list[i] == NULL) 
	 )
	/*INV-FIFO:	All tasks in a FIFO list are of 
				the same priority
	*/
	_(invariant (type==FIFO) ==> 
				( \forall unsigned i; 
					( (i<length) ==>
							(	\mine(list[i])  && 
								( list[i]->ownersPriority == priority) 
							) 
					)
				)
	 )
	/*INV-PQ:	All tasks in a PQ list are arranged in the 
				nondecreasing order of priority values
	*/
	_(invariant ( type==PQ )==>	
			(	\forall unsigned i , j; 
				(	( j < length ) && \mine(list[i]) && 
					\mine(list[j]) && ( i < j ) 
				) ==> (	list[i]->xItemValue <= 
						list[j]->xItemValue 
					  ) 
			) 
	 ) 
	/*INV-added:All valid items are contained in the list */
	_(invariant \forall xListItem *xli; ( \mine(xli) ) ==> 
		( xli->pvContainer==\this )  
	 )
	/*INV-added:For all valid items, the value of 
				ownersPriority is within the bound
	*/
	_(invariant \forall xListItem *xli; ( \mine(xli) ) ==> 
					( xli->ownersPriority <= maxNumVal ) 
	 )

	/*INV-added:For all valid list nodes 
				th eitem value is within the bound
	*/
	_(invariant \forall xListItem *xli; ( \mine(xli) ) ==> 
					( xli->xItemValue <= maxNumVal ) 
	 )

	/*INV-added: This structure owns 'maxNumVal' */
	_( invariant \mine( \embedding( &maxNumVal ) ) )

	/*INV-added: This structure owns 'maxPrio' */
	_( invariant \mine( \embedding( &maxPrio ) ) )

} xMap;



void listInitialiseItem(xListItem *li)
	_(requires \wrapped(li) )
	_(writes li )
	_(ensures li->pvContainer==NULL )
//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli != li ) ==>
					( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	//_(ensures \false)
	;


void setItemOwner(xListItem *li, TCB *task)
	_(requires \wrapped(li) )
	_(requires li->pvContainer==NULL )
	_(requires li->pvOwner==NULL )
	_(requires \wrapped(task) )
	_(writes li )
	_(writes task)
	_(ensures \wrapped(li) )
	_(ensures li->pvOwner==task )
	_(ensures li->ownersPriority == task->uxPriority )
//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	//_(ensures \false)
	;

void setItemValue(xListItem *li, unsigned value)
	_(requires \wrapped(li) )
	_(requires li->pvContainer==NULL )
	_(requires value<=maxNumVal )
	_(writes li )
	_(ensures \wrapped(li) )
	_(ensures li->xItemValue==value )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli == \old(xli) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
///////////////////////////////////////////////////////
	//_(ensures \false)
	;

unsigned getItemValue(xListItem *li)
	_(requires \wrapped(li) )
	_(ensures \result==li->xItemValue )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	//_(ensures \false)
	;


unsigned listIsEmpty(xMap *xList)
	_(requires \wrapped(xList) )
	_(ensures \result <==> xList->length==0 )
	_(ensures \wrapped(xList) )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	//_(ensures \false )
	;

unsigned currentLength(xMap *xList)
	_(requires \wrapped(xList) )
	_(ensures \result == xList->length )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	//_(ensures \false )
	;



TCB *getOwnerOfFirstEntry(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->type!=PQ )
	/*	Because this function is only for the FIFO queue*/
	_(requires xList->length>0 )
	_(ensures \result==xList->list[0]->pvOwner )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	//_(ensures \false )
	;


void rotateLeft(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->type!=PQ )
	/*	Because this function is only for the FIFO queue
		and it cannot restore the order of elements for PQ 
	*/
	_(requires ( xList->type==FIFO ) ==> 
		(\forall unsigned i; (i<xList->length) ==> 
					(	xList->list[i]->pvOwner->uxPriority	==	
						xList->priority 
					) 
		) 		
	 )
	_(requires xList->length>0 )
	_(writes xList)
	_(ensures \wrapped(xList) )
	_(ensures	xList->list[xList->length-1] ==
				\old(xList->list[0]) 
	 )
	_(ensures \forall  unsigned i; 
		( i < xList->length-1 ) ==> 
			( xList->list[i] == \old(xList->list[i+1]) ) 
	 ) 
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	//_(ensures \false )
	;


TCB* getOwnerOfNextEntry(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->type!=PQ )
	/*	Because this function is only for the FIFO queue
		and it cannot restore the order of elements for PQ 
	*/
	_(requires ( xList->type==FIFO ) ==> 
		(\forall unsigned i; (i<xList->length) ==> 
					(	xList->list[i]->pvOwner->uxPriority	==	
						xList->priority 
					) 
		) 		
	 )
	_(requires xList->length>0 )
	_(writes xList)
	_(ensures \wrapped(xList) )
	_(ensures \result==\old(xList->list[1]->pvOwner) )
	_(ensures	xList->list[xList->length-1] ==
				\old(xList->list[0]) 
	 )
	_(ensures \forall  unsigned i; 
		( i < xList->length-1 ) ==> 
			( xList->list[i] == \old(xList->list[i+1]) ) 
	 ) 
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	//_(ensures \false )
	;


TCB *getOwnerOfHeadEntry(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->length>0 )
	_(requires xList->list[0]->pvOwner->pvGenericListItem->
				ownersPriority <= maxPrio )
	_(ensures \result==xList->list[0]->pvOwner )
	_(ensures 
		\result->pvGenericListItem->ownersPriority <= maxPrio 
	 )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	//_(ensures \false )
	;

_(pure) unsigned containedWithin( xMap *xList, xListItem *li )
	_(requires \wrapped(xList) )
	_(requires \thread_local(li) ) 
	_(reads xList,li )

	_(ensures  \result ==
		(	( li \in xList->\owns ) 
		)
	 )

	//_(ensures \false )
	;

void listInitialise(xMap *xList _(ghost enum xListType type) )
	_(requires \mutable(xList) )
	_(requires xList->length == 0 )
	_(writes \span(xList) )
	_(ensures \wrapped(xList) )
	_(ensures xList->length == 0 )
	_(ensures xList->\owns=={} )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; ( xList != L ) ==> 
								L->type==\old(L->type) 
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==>
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==>
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
///////////////////////////////////////////////////////
	//_(ensures \false )
	;

void listInsertEnd(xMap *xList, xListItem *li)
	_(requires \wrapped(xList) )
	_(requires xList->type!=PQ )
	/*	 This function cannot restore the order 
		of elements for PQ
	*/
	_(requires ( xList->type==FIFO ) ==> (
			li->ownersPriority == xList->priority ) )
	_(requires \wrapped(li) )
	_(requires li->ownersPriority <= maxPrio )
	_(requires \forall unsigned i; 
		( i<xList->length ) ==> 
			(xList->list[i]->pvOwner!=li->pvOwner) 
	 )
	_(requires (xList->type==FIFO) ==>
		(\forall unsigned i; ( i<xList->length ) ==> 
				( xList->list[i]->pvOwner->uxPriority ==
								li->pvOwner->uxPriority 
				) 
		) 
	 )
	_(requires xList->length < maxNumVal )
	_(writes xList )
	_(writes li )
	_(ensures li->pvContainer == xList )
	_(ensures \forall unsigned i; 
		( i<\old(xList->length) ) ==> 
			( xList->list[i]==\old(xList->list[i]) ) 
	 )
	_(ensures xList->list[\old(xList->length)] == li )
	_(ensures xList->length == \old(xList->length+1) )
	_(ensures li \in xList->\owns )
	_(ensures \wrapped(xList) )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; 
								L->type==\old(L->type) 
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==>
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==>
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==>
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
	_(ensures xList->position[li] == xList->length )
	_(ensures \forall xListItem *xli; 
		(	( xli != li ) &&
			( xli \in xList->\owns )
		) ==> ( xList->position[ xli ] == \old(xList->position[ xli ]) )
	 )
	_(ensures xList->position[li] == xList->length  )
///////////////////////////////////////////////////////
	//_(ensures \false)
	;


void listInsert(xMap *xList, xListItem *li)
	_(requires \wrapped(xList) )
	_(requires \wrapped(li) )
	_(requires li->ownersPriority <= maxPrio )
	_(requires \forall unsigned i; 
		( i<xList->length ) ==> 
			 (xList->list[i]->pvOwner!=li->pvOwner ) 
	 )
	// This operation is only for priority queues
	_(requires ( xList->type== PQ ) )
	_(requires xList->length<maxNumVal )
	_(writes xList )
	_(writes li )
	_(ensures xList->length==\old(xList->length+1) )
	_(ensures xList->list[xList->position[li]] == li )
	_(ensures \forall unsigned i;
		(	( i < xList->length ) &&
			( i < xList->position[li] )
		) ==> ( xList->list[i] == \old(xList->list[i]) )
	 )
	_(ensures ( xList->list[xList->position[li]] == li ) )
	_(ensures \forall unsigned i;
		(	( i < xList->length ) &&
			( i > xList->position[li] )
		) ==> ( xList->list[i] == \old(xList->list[i-1]) )
	 )
	_(ensures li->pvContainer==xList )
	_(ensures li \in xList->\owns )
	_(ensures \wrapped(xList) )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; 
								L->type==\old(L->type) 
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
	_(ensures xList->position[li] == xList->length )
	_(ensures \forall xListItem *xli; 
		(	( xli != li ) &&
			( xli \in xList->\owns )
		) ==> ( xList->position[ xli ] == \old(xList->position[ xli ]) )
	 )
	_(ensures xList->position[li] == xList->length  )
///////////////////////////////////////////////////////
	//_(ensures \false)
	;

void listRemove(xMap *xList, xListItem *li)
	_(requires \wrapped(xList) )
	_(requires li \in xList->\owns )
	_(writes xList )
	_(ensures \wrapped(xList) )
	_(ensures xList->length == \old(xList->length-1) )
	_(ensures \forall unsigned i; 
		( i < \old(xList->position[\old(li)]) ) ==> 
			( xList->list[i]==\old(xList->list[i]) ) 
	 )
	_(ensures \forall unsigned i; 
		(	( i >= \old(xList->position[\old(li)]) ) && 
			( i < xList->length ) 
		) ==> ( xList->list[i] == \old(xList->list[i+1]) ) 
	 ) 
	_(ensures li->pvContainer == NULL )
	_(ensures \forall unsigned i; 
		( i<xList->length ) ==> ( xList->list[i] != li ) )
	_(ensures !(li \in xList->\owns) )
	_(ensures \wrapped(li) )
	_(ensures xList->\owns == \old(xList->\owns) - li )
	_(ensures \fresh(li) )	
	/*	To say explicitely that li's ownership is transferred 
		to the current thread. Because in VCC the ownership 
		transfer will be effected only when the 
		owner is closed.
	*/
	_(ensures ( xList->type == FIFO ) ==> 
			( xList->priority == \old(xList->priority) ) 
	 )
	_(ensures li->ownersPriority <= maxPrio )
	_(ensures \forall unsigned i;	
		(	( i < xList->length ) && 
			( xList->list[i] \in xList->\owns ) 
		) ==> ( (xList->list[i]->pvOwner != li->pvOwner ) ) 
	 )
	_(ensures xList->length < maxNumVal )  
	/*	The above is required to prove that there is a space 
		for insertion after every deletion
	*/
	_(ensures xList->position[li]== maxNumVal )
//////////////////////////////////////////////////////( li != li ) ==>
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; 
								L->type==\old(L->type) 
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
///////////////////////////////////////////////////////
	//_(ensures \false)
	;