Data Science 523 - Assignment #2 -- Fall 2020

Due: Friday 6 November 2020, Before Class

Write a formal spec for seating in an airplane:

• An airplane has 100 seats (1..100)
• Every passenger gets one seat
• Any seat with a passenger holds only one passenger
• The state of a plane P is a function [N -> S]
  • Maps a passenger name to a seat number
• Two functions: assign_seat and deassign_seat
• Define the functions
• Show some lemmas that demonstrate correctness

Start of Homework Solution:

• Types:
  • N : type (of passenger)
  • S : type (of seat number)
  • A : type (of airplane function) [N -> S]
  • e0 : N (represents an empty seat)
• Variables:
  • nm : var N (a passenger)
  • pl : var A (an airplane function)
  • st : var S (a seat number)

What you Need to Do:

1. Define the axioms for the two functions:
   • assign_seat : [A x N x S -> A]
   • deassign_seat : [A x S -> A]
2. Be careful that the spec covers all requirements:
   • Can someone have “e0” as their seat number?
   • Can a passenger have more than one seat?
   • Can a seat have more than one passenger?
3. Identify some lemmas that demonstrate that the system specification describes what is intended and sketch the proof

See Rushby, PVS Phone Book Example for an example of a different problem that requires a similar specticiation.

Submit your assignment using the Assignment 2 Dropbox in D2L for DSci523 Fall 2020.