author  nipkow 
Thu, 22 Jul 2004 17:37:31 +0200  
changeset 15074  277b3a4da341 
parent 11786  51ce34ef5113 
child 17310  1322ed8e0ee4 
permissions  rwrr 
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

1 
(* Title: HOL/UNITY/Alloc 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

2 
ID: $Id$ 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

4 
Copyright 1998 University of Cambridge 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

5 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

6 
Specification of Chandy and Charpentier's Allocator 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

7 
*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

8 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

9 
Alloc = AllocBase + PPROD + 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

10 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

11 
(** State definitions. OUTPUT variables are locals **) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

12 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

13 
record clientState = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

14 
giv :: nat list (*client's INPUT history: tokens GRANTED*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

15 
ask :: nat list (*client's OUTPUT history: tokens REQUESTED*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

16 
rel :: nat list (*client's OUTPUT history: tokens RELEASED*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

17 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

18 
record 'a clientState_d = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

19 
clientState + 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

20 
dummy :: 'a (*dummy field for new variables*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

21 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

22 
constdefs 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

23 
(*DUPLICATED FROM Client.thy, but with "tok" removed*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

24 
(*Maybe want a special theory section to declare such maps*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

25 
non_dummy :: 'a clientState_d => clientState 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

26 
"non_dummy s == (giv = giv s, ask = ask s, rel = rel s)" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

27 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

28 
(*Renaming map to put a Client into the standard form*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

29 
client_map :: "'a clientState_d => clientState*'a" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

30 
"client_map == funPair non_dummy dummy" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

31 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

32 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

33 
record allocState = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

34 
allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

35 
allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

36 
allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

37 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

38 
record 'a allocState_d = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

39 
allocState + 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

40 
dummy :: 'a (*dummy field for new variables*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

41 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

42 
record 'a systemState = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

43 
allocState + 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

44 
client :: nat => clientState (*states of all clients*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

45 
dummy :: 'a (*dummy field for new variables*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

46 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

47 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

48 
constdefs 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

49 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

50 
(** Resource allocation system specification **) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

51 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

52 
(*spec (1)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

53 
system_safety :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

54 
"system_safety == 
15074  55 
Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s) 
56 
<= NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}" 

11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

57 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

58 
(*spec (2)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

59 
system_progress :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

60 
"system_progress == INT i : lessThan Nclients. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

61 
INT h. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

62 
{s. h <= (ask o sub i o client)s} LeadsTo 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

63 
{s. h pfixLe (giv o sub i o client) s}" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

64 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

65 
system_spec :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

66 
"system_spec == system_safety Int system_progress" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

67 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

68 
(** Client specification (required) ***) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

69 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

70 
(*spec (3)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

71 
client_increasing :: 'a clientState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

72 
"client_increasing == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

73 
UNIV guarantees Increasing ask Int Increasing rel" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

74 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

75 
(*spec (4)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

76 
client_bounded :: 'a clientState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

77 
"client_bounded == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

78 
UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

79 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

80 
(*spec (5)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

81 
client_progress :: 'a clientState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

82 
"client_progress == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

83 
Increasing giv guarantees 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

84 
(INT h. {s. h <= giv s & h pfixGe ask s} 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

85 
LeadsTo {s. tokens h <= (tokens o rel) s})" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

86 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

87 
(*spec: preserves part*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

88 
client_preserves :: 'a clientState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

89 
"client_preserves == preserves giv Int preserves clientState_d.dummy" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

90 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

91 
(*environmental constraints*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

92 
client_allowed_acts :: 'a clientState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

93 
"client_allowed_acts == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

94 
{F. AllowedActs F = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

95 
insert Id (UNION (preserves (funPair rel ask)) Acts)}" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

96 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

97 
client_spec :: 'a clientState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

98 
"client_spec == client_increasing Int client_bounded Int client_progress 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

99 
Int client_allowed_acts Int client_preserves" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

100 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

101 
(** Allocator specification (required) ***) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

102 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

103 
(*spec (6)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

104 
alloc_increasing :: 'a allocState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

105 
"alloc_increasing == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

106 
UNIV guarantees 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

107 
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

108 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

109 
(*spec (7)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

110 
alloc_safety :: 'a allocState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

111 
"alloc_safety == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

112 
(INT i : lessThan Nclients. Increasing (sub i o allocRel)) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

113 
guarantees 
15074  114 
Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s) 
115 
<= NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}" 

11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

116 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

117 
(*spec (8)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

118 
alloc_progress :: 'a allocState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

119 
"alloc_progress == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

120 
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

121 
Increasing (sub i o allocRel)) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

122 
Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

123 
Always {s. ALL i<Nclients. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

124 
ALL elt : set ((sub i o allocAsk) s). elt <= NbT} 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

125 
Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

126 
(INT i : lessThan Nclients. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

127 
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

128 
LeadsTo 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

129 
{s. tokens h <= (tokens o sub i o allocRel)s}) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

130 
guarantees 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

131 
(INT i : lessThan Nclients. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

132 
INT h. {s. h <= (sub i o allocAsk) s} 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

133 
LeadsTo 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

134 
{s. h pfixLe (sub i o allocGiv) s})" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

135 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

136 
(*NOTE: to follow the original paper, the formula above should have had 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

137 
INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s} 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

138 
LeadsTo 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

139 
{s. tokens h i <= (tokens o sub i o allocRel)s}) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

140 
thus h should have been a function variable. However, only h i is ever 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

141 
looked at.*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

142 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

143 
(*spec: preserves part*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

144 
alloc_preserves :: 'a allocState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

145 
"alloc_preserves == preserves allocRel Int preserves allocAsk Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

146 
preserves allocState_d.dummy" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

147 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

148 
(*environmental constraints*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

149 
alloc_allowed_acts :: 'a allocState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

150 
"alloc_allowed_acts == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

151 
{F. AllowedActs F = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

152 
insert Id (UNION (preserves allocGiv) Acts)}" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

153 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

154 
alloc_spec :: 'a allocState_d program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

155 
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

156 
alloc_allowed_acts Int alloc_preserves" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

157 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

158 
(** Network specification ***) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

159 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

160 
(*spec (9.1)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

161 
network_ask :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

162 
"network_ask == INT i : lessThan Nclients. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

163 
Increasing (ask o sub i o client) guarantees 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

164 
((sub i o allocAsk) Fols (ask o sub i o client))" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

165 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

166 
(*spec (9.2)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

167 
network_giv :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

168 
"network_giv == INT i : lessThan Nclients. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

169 
Increasing (sub i o allocGiv) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

170 
guarantees 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

171 
((giv o sub i o client) Fols (sub i o allocGiv))" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

172 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

173 
(*spec (9.3)*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

174 
network_rel :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

175 
"network_rel == INT i : lessThan Nclients. 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

176 
Increasing (rel o sub i o client) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

177 
guarantees 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

178 
((sub i o allocRel) Fols (rel o sub i o client))" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

179 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

180 
(*spec: preserves part*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

181 
network_preserves :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

182 
"network_preserves == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

183 
preserves allocGiv Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

184 
(INT i : lessThan Nclients. preserves (rel o sub i o client) Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

185 
preserves (ask o sub i o client))" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

186 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

187 
(*environmental constraints*) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

188 
network_allowed_acts :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

189 
"network_allowed_acts == 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

190 
{F. AllowedActs F = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

191 
insert Id 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

192 
(UNION (preserves allocRel Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

193 
(INT i: lessThan Nclients. preserves(giv o sub i o client))) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

194 
Acts)}" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

195 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

196 
network_spec :: 'a systemState program set 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

197 
"network_spec == network_ask Int network_giv Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

198 
network_rel Int network_allowed_acts Int 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

199 
network_preserves" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

200 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

201 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

202 
(** State mappings **) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

203 
sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

204 
"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

205 
in ( allocGiv = allocGiv s, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

206 
allocAsk = allocAsk s, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

207 
allocRel = allocRel s, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

208 
client = cl, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

209 
dummy = xtr)" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

210 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

211 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

212 
sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

213 
"sysOfClient == %(cl,al). ( allocGiv = allocGiv al, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

214 
allocAsk = allocAsk al, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

215 
allocRel = allocRel al, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

216 
client = cl, 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

217 
systemState.dummy = allocState_d.dummy al)" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

218 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

219 
consts 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

220 
Alloc :: 'a allocState_d program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

221 
Client :: 'a clientState_d program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

222 
Network :: 'a systemState program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

223 
System :: 'a systemState program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

224 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

225 
rules 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

226 
Alloc "Alloc : alloc_spec" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

227 
Client "Client : client_spec" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

228 
Network "Network : network_spec" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

229 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

230 
defs 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

231 
System_def 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

232 
"System == rename sysOfAlloc Alloc Join Network Join 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

233 
(rename sysOfClient 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

234 
(plam x: lessThan Nclients. rename client_map Client))" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

235 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

236 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

237 
(** 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

238 
locale System = 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

239 
fixes 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

240 
Alloc :: 'a allocState_d program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

241 
Client :: 'a clientState_d program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

242 
Network :: 'a systemState program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

243 
System :: 'a systemState program 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

244 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

245 
assumes 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

246 
Alloc "Alloc : alloc_spec" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

247 
Client "Client : client_spec" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

248 
Network "Network : network_spec" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

249 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

250 
defines 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

251 
System_def 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

252 
"System == rename sysOfAlloc Alloc 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

253 
Join 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

254 
Network 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

255 
Join 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

256 
(rename sysOfClient 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

257 
(plam x: lessThan Nclients. rename client_map Client))" 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

258 
**) 
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

259 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

260 

ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

261 
end 