Exercises: Developing and Proving Algorithms with PVS (Part II)

Consider the theories UTM0, UTM, and the lecture Developing and Proving Algorithms with PVS (Part II).

1. Write a strategy called uss-tcc and use it to discharge the proofs of subscribe_j, test_0, test_1, Dos, and test_update. Hint: The strategy does the following: first apply grind, then to each generated subgoal, expand exists_op as many times as needed.
2. Define the function in_operational_volume?(uss:USS)(p:Vect3) : bool that returns TRUE if the point p is inside the operational volume of uss. Hint: Check that:
   • The vertical component of p, i.e., p`z, is below uss`op_alt.
   • The horizontal component of p, i.e., vect2(p), is inside uss`op_area.
   • Look for the names of the functions in NASALib/shapes that check if a point is inside a circle, rectangle, and triangle.
3. Define the function check_flight_plan(uss:USS,ac_id:AircraftId) that returns:
   • NotFound, if the aircraft ac_id is not in uss;
   • OK, if the aircraft is in uss and every waypoint in its flight plan lies inside the USS operational volume;
   • Failure(wps) otherwise, where wps is the list of waypoints in its flight plan that lie outside the USS operational volume.