Verifying goto (succeeding)
Verifying example with goto's and labels. We verify a program with goto's to skip certain code fragments, and show that these fragments do not update the code in some way.
|Path to example file||goto/goto2.pvl|
|Lines of code||16 lines (comments not included)|
|Lines of specification||2 lines (12.5% of the total)|
|Computation time||17038 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.