Demonstrating SPARK with a Mars Rover (Part 2): The Safety Property

Now, SPARK says that the first Loop Invariant, where “Cmd = Last_Cmd”, fails on the first iteration. Therefore, the if statement containing the case statement with the Rover commands can be ignored in our debugging. Let’s talk through how the “Run” procedure works again, with this…