# HG changeset patch
# User paulson
# Date 929010979 -7200
# Node ID de4d358bf01e7b49d3f15833bfed2e526af69111
# Parent  d96d4977f94ee5b530b5804dc06418385700246e
The Allocator example: specifications

diff -r d96d4977f94e -r de4d358bf01e src/HOL/UNITY/Alloc.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Alloc.ML	Thu Jun 10 12:36:19 1999 +0200
@@ -0,0 +1,1 @@
+Addsimps [sub_def];
diff -r d96d4977f94e -r de4d358bf01e src/HOL/UNITY/Alloc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Alloc.thy	Thu Jun 10 12:36:19 1999 +0200
@@ -0,0 +1,143 @@
+(*  Title:      HOL/UNITY/Alloc
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Specification of Chandy and Charpentier's Allocator
+*)
+
+Alloc = Follows + Comp +
+
+(*simplifies the expression of some specifications*)
+constdefs
+  sub :: ['a, 'a=>'b] => 'b
+    "sub i f == f i"
+
+(*Duplicated from HOL/ex/NatSum.thy.
+  Maybe type should be  [nat=>int, nat] => int**)
+consts sum     :: [nat=>nat, nat] => nat
+primrec 
+  "sum f 0 = 0"
+  "sum f (Suc n) = f(n) + sum f n"
+
+
+(*This function merely sums the elements of a list*)
+consts tokens     :: nat list => nat
+primrec 
+  "tokens [] = 0"
+  "tokens (x#xs) = x + tokens xs"
+
+
+consts
+  NbT      :: nat       (*Number of tokens in system*)
+  Nclients :: nat       (*Number of clients*)
+
+
+record clientState =
+  giv :: nat list   (*client's INPUT history:  tokens GRANTED*)
+  ask :: nat list   (*client's OUTPUT history: tokens REQUESTED*)
+  rel :: nat list   (*client's OUTPUT history: tokens RELEASED*)
+
+record allocState =
+  allocGiv :: nat => nat list   (*allocator's local copy of "giv" for i*)
+  allocAsk :: nat => nat list   (*allocator's local copy of "ask" for i*)
+  allocRel :: nat => nat list   (*allocator's local copy of "rel" for i*)
+
+record systemState = allocState +
+  client :: nat => clientState  (*states of all clients*)
+
+
+constdefs
+
+(** Resource allocation system specification **)
+
+  (*spec (1)*)
+  system_safety :: systemState program set
+    "system_safety ==
+     Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients
+	        <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}"
+
+  (*spec (2)*)
+  system_progress :: systemState program set
+    "system_progress == INT i : lessThan Nclients.
+			INT h. 
+			  {s. h <= (ask o sub i o client)s} LeadsTo
+			  {s. h pfix_le (giv o sub i o client) s}"
+
+(** Client specification (required) ***)
+
+  (*spec (3)*)
+  client_increasing :: clientState program set
+    "client_increasing ==
+         UNIV guarantees Increasing ask Int Increasing rel"
+
+  (*spec (4)*)
+  client_bounded :: clientState program set
+    "client_bounded ==
+         UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
+
+  (*spec (5)*)
+  client_progress :: clientState program set
+    "client_progress ==
+	 Increasing giv
+	 guarantees
+	 (INT h. {s. h <= giv s & h pfix_ge ask s}
+		 LeadsTo
+		 {s. tokens h <= (tokens o rel) s})"
+
+(** Allocator specification (required) ***)
+
+  (*spec (6)*)
+  alloc_increasing :: allocState program set
+    "alloc_increasing ==
+	 UNIV
+         guarantees
+	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk))"
+
+  (*spec (7)*)
+  alloc_safety :: allocState program set
+    "alloc_safety ==
+	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
+         guarantees
+	 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
+	         <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
+
+  (*spec (8)*)
+  alloc_progress :: allocState program set
+    "alloc_progress ==
+	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
+	                             Increasing (sub i o allocRel))
+         Int
+         Always {s. ALL i : lessThan Nclients.
+		    ALL k : lessThan (length (allocAsk s i)).
+		    allocAsk s i ! k <= NbT}
+         Int
+         (INT i : lessThan Nclients. 
+	  INT h. {s. h <= (sub i o allocGiv)s & h pfix_ge (sub i o allocAsk)s}
+		  LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
+         guarantees
+	     (INT i : lessThan Nclients.
+	      INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
+	             {s. h pfix_le (sub i o allocGiv) s})"
+
+(** Network specification ***)
+
+  (*spec (9.1)*)
+  network_ask :: systemState program set
+    "network_ask == INT i : lessThan Nclients.
+                    Increasing (ask o sub i o client) guarantees
+                    ((sub i o allocAsk) Fols (ask o sub i o client))"
+
+  (*spec (9.2)*)
+  network_giv :: systemState program set
+    "network_giv == INT i : lessThan Nclients.
+                    Increasing (sub i o allocGiv) guarantees
+                    ((giv o sub i o client) Fols (sub i o allocGiv))"
+
+  (*spec (9.3)*)
+  network_rel :: systemState program set
+    "network_rel == INT i : lessThan Nclients.
+                    Increasing (rel o sub i o client) guarantees
+                    ((sub i o allocRel) Fols (rel o sub i o client))"
+
+end