changeset 48907 | 5c4275c3b5b8 |
parent 47152 | 446cfc760ccf |
child 50662 | b1f4291eb916 |
48906:5b192d6b7a54 | 48907:5c4275c3b5b8 |
---|---|
4 |
4 |
5 header {* Boogie example: Dijkstra's algorithm *} |
5 header {* Boogie example: Dijkstra's algorithm *} |
6 |
6 |
7 theory Boogie_Dijkstra |
7 theory Boogie_Dijkstra |
8 imports Boogie |
8 imports Boogie |
9 uses ("Boogie_Dijkstra.b2i") |
|
10 begin |
9 begin |
11 |
10 |
12 text {* |
11 text {* |
13 We prove correct the verification condition generated from the following |
12 We prove correct the verification condition generated from the following |
14 Boogie code: |
13 Boogie code: |