equal
deleted
inserted
replaced
1224 know whether this includes also code for proofs). Our formalisation |
1224 know whether this includes also code for proofs). Our formalisation |
1225 consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar |
1225 consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar |
1226 code with a few apply-scripts interspersed. The formal model of PIP |
1226 code with a few apply-scripts interspersed. The formal model of PIP |
1227 is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary |
1227 is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary |
1228 definitions and proofs took 770 lines of code. The properties relevant |
1228 definitions and proofs took 770 lines of code. The properties relevant |
1229 for an implementation took 2000 lines. Our code can be downloaded from |
1229 for an implementation took 2000 lines. %%Our code can be downloaded from |
1230 ... |
1230 %%... |
1231 |
1231 |
1232 \bibliographystyle{plain} |
1232 \bibliographystyle{plain} |
1233 \bibliography{root} |
1233 \bibliography{root} |
1234 *} |
1234 *} |
1235 |
1235 |