//*******************************************************
//* File:    /Aircraft.pd
//* Author:  UP696771
//* License: See /LICENSE
//* For full list of assumptions, please see /assumptions.txt
//*******************************************************
import "Utils.pd";

class Aircraft ^=
abstract
	var 
		type : string,
		passengerLimit : nat;
	
	invariant
		#type = 3 | #type = 4, // ICAO D-8643 Aircraft Type Designators are 3 or 4 letter universally unique identifiers
		isAlpha@Utils(type); // D-8643 codes are alphanumeric
		
interface
	function 
		type,
		passengerLimit;
		
	build{!type:string, !passengerLimit:nat}
		pre (#type = 3 | #type = 4) & isAlpha@Utils(type);
end;