equal
deleted
inserted
replaced
1184 processes are not independent, but coordinated via a master |
1184 processes are not independent, but coordinated via a master |
1185 process that distributes work over some slave processes. However a |
1185 process that distributes work over some slave processes. However a |
1186 formal investigation of this is beyond the scope of this paper. |
1186 formal investigation of this is beyond the scope of this paper. |
1187 We are not aware of any proofs in this area, not even informal ones. |
1187 We are not aware of any proofs in this area, not even informal ones. |
1188 |
1188 |
1189 Our formalisation consists of X lines of readable Isabelle/Isar code, with some |
1189 Our formalisation consists of 6894 of readable Isabelle/Isar code, with some |
1190 apply-scripts interspersed. The formal model is Y lines long; the |
1190 apply-scripts interspersed. The formal model is 385 lines long; the |
1191 formal correctness proof Z lines. The properties relevant for an |
1191 formal correctness proof 3777 lines. The properties relevant for an |
1192 implementation are U lines long. |
1192 implementation are 1964 lines long; Auxlliary definitions and notions are |
|
1193 768 lines. |
|
1194 |
1193 |
1195 |
1194 *} |
1196 *} |
1195 |
1197 |
1196 section {* Key properties \label{extension} *} |
1198 section {* Key properties \label{extension} *} |
1197 |
1199 |