A simple seat reservation system is specified and then verified in Mizar. The example was first introduced in:
and then reused with some extensions in:
There are three versions of the Mizar specification.
PC Mizar, Version 7.5.01 (Linux/FPC).
Not all Mizar articles that I use are in the Main Mizar Library (MML)
at the moment. Here is the abstract of mspf_1.
All the Mizar sources and abstracts are here.
Reading Mizar texts can be quite a struggle for newcomers, like with all other formal systems. Some knowledge of MML and access to MML can be helpful. The seat reservation system seems to be a good example for a tutorial on some aspects of Mizar.
Flights, seats, etc. All the sets Flights, Planes, Preference, and Passengers are introduced as non empty sets, this was required for some definitions. row and position are introduced as non empty sets without saying that they are initial segments of positive numbers. Then the set Seats is their Cartesian product.
Seat assignment. The cartesian product of Seats and Passengers is called seat_assignments. The selector functors seat and pass are then defined for a seat assignment. The set of flight_assignments is defined as the powerset (bool) of seat_assignments.
Flight data base is defined as a function from Flights to flight_assignments. The value of this function on a particular flight can be then seen as a binary relation with its domain in Seats and its range in Passengers. initial_state is a flight data base with empty flight assignment for each flight.
Attributes of airplanes. Since Mizar does not permit to introduce uninterpreted predicates, we first introduce sets Seat_exists and Meets_pref, and then define corresponding predicates.
Next seat. Mizar does not permit to introduce functions and then define their properties axiomatically as is done in [1] and [2]. The function Next_seat with the required properties was therefore constructed. I had to change the definiens of pref_filled to include also the condition that the relevant seats exist in respective airplanes. (Note that meets_pref pl, se, pref can be true even if the seat se does not exist on the plane pl) First, the function Ns_choice is defined that returns the seats on a given flight that satisfy the given preference. The definition is permissive meaning that the definiens is accessible only when the definitional condition is satisfied. The function Next_seat (also permissive) is then defined to return one of the existing seats (choose is the choice operator). The expected properties of Next_seat are stated in a theorem. It is worthwhile noticing that one of the axioms assumed in [1](p. 51) and in [2] (now corrected p. 7) about their uninterpreted function Next_seat was too strong (false).
Operations. The definitions of Cancel_assn, Make_assn and Look_up are essentially the same as in [2]. In the definiens of Look_up I had to play with type casting as processing of the Fraenkel operator in Mizar is not automated.
Invariants. After introducing appropriate notations all the invariants are proven.
Putative theorems. All the putative theorems are proven in turn. The Lp2_lem has been reformulated a bit.
Conclusions. Mizar proofs are much longer than the corresponding instructions for the PVS prover. I am impressed by the grinding power of PVS.
Remark. In Mizar, I have to type the proof, in PVS, I have to read the intermediate states of the prover. The latter is not necessarily a very pleasant task (that the former can be painful I know very well).
Here are the definitions and theorems without proofs . @proof means that the proof is not checked.
Seats. The function Seats_on_plane is a family of uninterpreted sets (indexed by Planes) resulting in seats available on a specific plane. Meets_pref is a family of functions (indexed by Planes) resulting in functions that to each preference give the set of seats on the plane meeting the preference. Seats_on_flight is analogous to Seats_on_plane but indexed by the Flights.
Flight data base is defined as a family of one-to-one partial functions (indexed by Flights) which to each flight assign a partial function from the set of seats on the plane of this flight into Passengers. The initial data base is a family of empty functions.
Next seat. The Next_Seat function is constructed using an auxiliary function Flight_Pref. The required properties of Next_seat are then proven.
Operations. The operations Cancel_assn and Make_assn are proven to return proper flight data base type. The Look_up is defined in terms of the inverse of seat assignments.
Invariants There is almost nothing to prove as the required invariants follow from typing. This is the main gain from using richer types. The invariants of operations are expressed in the type of their result. There is a guarantee that we do not forget to prove an invariant for an operation as it must be done when the operation is defined.
Putative theorems have been proven, they are expressed slightly differently than in Version 0.
Here are the definitions and theorems without proofs . @proof means that the proof is not checked. .
With this approach I would be able also to introduce operations like: add a flight, add a plane, etc but I have not done so.
Here is the abstract of the Mizar article, which has been automatically generated from the full Mizar text. An automatic generation of Mizar abstracts was imposiible for the previous versions because of the non-exportable objects.
The complete Mizar text . Note: the proofs are almost identical to Version 1.