src/HOL/UNITY/Alloc.thy
author paulson
Thu, 28 Oct 1999 16:04:57 +0200
changeset 7962 d139b03fcac2
parent 7630 d0e4a6f1f05c
child 8041 e3237d8c18d6
permissions -rw-r--r--
tidied
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Alloc
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
     2
    ID:         $Id$
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
     5
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
     6
Specification of Chandy and Charpentier's Allocator
7537
875754b599df working snapshot
paulson
parents: 7361
diff changeset
     7
875754b599df working snapshot
paulson
parents: 7361
diff changeset
     8
CONSIDER CHANGING "sum" to work on type "int", not "nat"
875754b599df working snapshot
paulson
parents: 7361
diff changeset
     9
  --then can use subtraction in spec (1),
875754b599df working snapshot
paulson
parents: 7361
diff changeset
    10
  --but need invariants that values are non-negative
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    11
*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    12
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents: 7540
diff changeset
    13
Alloc = Follows + Project + PPROD +
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    14
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    15
(*Duplicated from HOL/ex/NatSum.thy.
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    16
  Maybe type should be  [nat=>int, nat] => int**)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    17
consts sum     :: [nat=>nat, nat] => nat
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    18
primrec 
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    19
  "sum f 0 = 0"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    20
  "sum f (Suc n) = f(n) + sum f n"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    21
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    22
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    23
(*This function merely sums the elements of a list*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    24
consts tokens     :: nat list => nat
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    25
primrec 
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    26
  "tokens [] = 0"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    27
  "tokens (x#xs) = x + tokens xs"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    28
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    29
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    30
consts
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    31
  NbT      :: nat       (*Number of tokens in system*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    32
  Nclients :: nat       (*Number of clients*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    33
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    34
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    35
record clientState =
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    36
  giv :: nat list   (*client's INPUT history:  tokens GRANTED*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    37
  ask :: nat list   (*client's OUTPUT history: tokens REQUESTED*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    38
  rel :: nat list   (*client's OUTPUT history: tokens RELEASED*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    39
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    40
record allocState =
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    41
  allocGiv :: nat => nat list   (*allocator's local copy of "giv" for i*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    42
  allocAsk :: nat => nat list   (*allocator's local copy of "ask" for i*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    43
  allocRel :: nat => nat list   (*allocator's local copy of "rel" for i*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    44
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    45
record systemState = allocState +
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    46
  client :: nat => clientState  (*states of all clients*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    47
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    48
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    49
constdefs
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    50
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    51
(** Resource allocation system specification **)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    52
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    53
  (*spec (1)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    54
  system_safety :: systemState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    55
    "system_safety ==
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    56
     Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    57
	        <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    58
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    59
  (*spec (2)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    60
  system_progress :: systemState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    61
    "system_progress == INT i : lessThan Nclients.
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    62
			INT h. 
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    63
			  {s. h <= (ask o sub i o client)s} LeadsTo
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    64
			  {s. h pfixLe (giv o sub i o client) s}"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    65
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    66
  system_spec :: systemState program set
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    67
    "system_spec == system_safety Int system_progress"
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    68
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    69
(** Client specification (required) ***)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    70
7347
ad0ce67e4eb6 another snapshot
paulson
parents: 7188
diff changeset
    71
  (*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    72
  client_increasing :: clientState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    73
    "client_increasing ==
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
    74
         UNIV guarantees Increasing ask Int Increasing rel"
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    75
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    76
  (*spec (4)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    77
  client_bounded :: clientState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    78
    "client_bounded ==
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
    79
         UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    80
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    81
  (*spec (5)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    82
  client_progress :: clientState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    83
    "client_progress ==
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    84
	 Increasing giv
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
    85
	 guarantees
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    86
	 (INT h. {s. h <= giv s & h pfixGe ask s}
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    87
		 LeadsTo
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    88
		 {s. tokens h <= (tokens o rel) s})"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    89
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    90
  client_spec :: clientState program set
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    91
    "client_spec == client_increasing Int client_bounded Int client_progress"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
    92
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    93
(** Allocator specification (required) ***)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    94
7347
ad0ce67e4eb6 another snapshot
paulson
parents: 7188
diff changeset
    95
  (*spec (6)  PROBABLY REQUIRES A LOCALTO PRECONDITION*)
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    96
  alloc_increasing :: allocState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    97
    "alloc_increasing ==
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
    98
	 UNIV
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
    99
         guarantees
7540
8af61a565a4a working Safety proof for the system at last
paulson
parents: 7537
diff changeset
   100
	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   101
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   102
  (*spec (7)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   103
  alloc_safety :: allocState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   104
    "alloc_safety ==
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   105
	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
   106
         guarantees
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   107
	 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   108
	         <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   109
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   110
  (*spec (8)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   111
  alloc_progress :: allocState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   112
    "alloc_progress ==
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   113
	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   114
	                             Increasing (sub i o allocRel))
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   115
         Int
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   116
         Always {s. ALL i : lessThan Nclients.
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   117
		    ALL k : lessThan (length (allocAsk s i)).
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   118
		    allocAsk s i ! k <= NbT}
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   119
         Int
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   120
         (INT i : lessThan Nclients. 
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   121
	  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   122
		  LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
   123
         guarantees
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   124
	     (INT i : lessThan Nclients.
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   125
	      INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   126
	             {s. h pfixLe (sub i o allocGiv) s})"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   127
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   128
  alloc_spec :: allocState program set
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   129
    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress"
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   130
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   131
(** Network specification ***)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   132
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   133
  (*spec (9.1)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   134
  network_ask :: systemState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   135
    "network_ask == INT i : lessThan Nclients.
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   136
                    Increasing (ask o sub i o client)
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
   137
                    guarantees
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   138
                    ((sub i o allocAsk) Fols (ask o sub i o client))"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   139
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   140
  (*spec (9.2)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   141
  network_giv :: systemState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   142
    "network_giv == INT i : lessThan Nclients.
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   143
                    Increasing (sub i o allocGiv)
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
   144
                    guarantees
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   145
                    ((giv o sub i o client) Fols (sub i o allocGiv))"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   146
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   147
  (*spec (9.3)*)
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   148
  network_rel :: systemState program set
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   149
    "network_rel == INT i : lessThan Nclients.
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   150
                    Increasing (rel o sub i o client)
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7347
diff changeset
   151
                    guarantees
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   152
                    ((sub i o allocRel) Fols (rel o sub i o client))"
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   153
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   154
  network_spec :: systemState program set
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   155
    "network_spec == network_ask Int network_giv Int network_rel"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   156
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   157
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   158
(** State mappings **)
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   159
  sysOfAlloc :: "(allocState * (nat => clientState)) => systemState"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   160
    "sysOfAlloc == %(s,y). (| allocGiv = allocGiv s,
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   161
			      allocAsk = allocAsk s,
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   162
			      allocRel = allocRel s,
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   163
			      client   = y |)"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   164
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   165
  sysOfClient :: "((nat => clientState) * allocState ) => systemState"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   166
    "sysOfClient == %(x,y). sysOfAlloc(y,x)"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   167
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   168
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   169
locale System =
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   170
  fixes 
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   171
    Alloc   :: allocState program
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   172
    Client  :: clientState program
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   173
    Network :: systemState program
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   174
    System  :: systemState program
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   175
  
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   176
  assumes
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   177
    Alloc   "Alloc   : alloc_spec"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   178
    Client  "Client  : client_spec"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   179
    Network "Network : network_spec"
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   180
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   181
  defines
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   182
    System_def
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   183
      "System == (extend sysOfAlloc Alloc)
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   184
                 Join
6841
5a557122bb62 renamed PPI to plam
paulson
parents: 6837
diff changeset
   185
                 (extend sysOfClient (plam x: lessThan Nclients. Client))
6827
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   186
                 Join
b69a2585ec0f guar; locale for the spec
paulson
parents: 6815
diff changeset
   187
                 Network"
6815
de4d358bf01e The Allocator example: specifications
paulson
parents:
diff changeset
   188
end