(******************************************************************************
 ****       This RSL file is an example specification from CSC 440        ****
 **** The companion derived design is in ../../examples/restaurant/design ****
 ******************************************************************************)


(*****
 **** OBJECTS
 *****)

object RestaurantDB
    components: fm:FoodMenu and fsi:FoodStuffsInventory and 
	bl:MenuItemBreakdowns and pw:Password;
    operations: MaintainDB;
    description: (*
	The RestaurantDB is the repository of all electronic restaurant
	information.  The three main components are the menus seen by the
	customer, the food stuffs inventory that records all current stock on
	hand, and the menu item breakdowns that describes the food stuffs that
	each menu item is composed of.  The Password is the currently legal
	password that must be known by a user before access to the database is
	allowed.  The password is set using the EnterPassword operation.
    *);
end RestaurantDB;

object SecureDB
    components: av:AccessValidation;
    description: (*
	This is the superclass for any database that requires secure access.
	The intent of the AccessValidation component is that it be set to true
	whenever a user is validated.  In the restaurant system, access
	validation is set true in the ValidateUser operation.
    *);
end SecureDB;

object Password =  string;
object AccessValidation =  boolean;


(**
 * The next several objects define the food menu seen by customers.
 **)
object FoodMenu extends SecureDB
    components: MenuSection*;
    operations: AddSection, DelSection, ChangeSection;
    description: (*
	The FoodMenu is the top-level structure of menu seen by the customer
	from which order selections are made.  It is composed of a number of
	MenuSections.  The standard menu sections are Hamburgers, Drinks, and
	Side Orders.
    *);
end FoodMenu;

object MenuSection
    components: Name and MenuItem*;
    description: (*
	Each MenuSection of the menu consists of a list of indivdual menu
	items.  For example, the hamburgers section contains a menu item for
	each of the different kinds of hamburgers
    *);
end MenuSection;

object MenuItem
    components: Name and Description and Price and MenuItemAccessories;
    description: (*
	Each MenuItem in a MenuSection has the listed components.  Four
	example, a MenuItem for a plain hamburger is the following:

		Name: "Plain Hamburger"
		Description: "1/4 LB patty on a sesame seed bun"
		Price: "$1.89"
		Accessories: "Mayonaise", "Mustard", "Catsup", "Lettuce",
			"Tomato", "Pickles", "Onion", "Cheese", "Mushrooms"

	Note that the list of accessories includes an indication of whether a
	particular extra is or is not normally included, which detail is not
	shown here.  See the definition of the Accessories object below for
	details.
    *);
end MenuItem;

object MenuItemAccessories
    components: MenuItemAccessory*;
    description: (*
	This is the list of accessory items that can appear with a MenuItem.
	Accessories is also a component of the MenuItemBreakdown object defined
	farther below.
    *);
end MenuItemAccessories;

object MenuItemAccessory
    components: Name and IsStandard and Price;
    description: (*

	Each MenuItemAccessory has a name, an indication as to whether it is
	standard, and a price.  For example, here is the structure of a
	mayonaise accessory for a standard hamburger:

		Name: "Mayonaise"
		IsStandard: true
		Price: 0

	This example indicates that Mayonaise is standard, and there is no
	charge for it.  If a MenuItemAccessory is standard, then it is normally
	included on a menu item unless the customer explicitly requests that it
	be removed.  The converse is true for non-standard a MenuItemAccessory.

	See also the ItemOrderAccessory object below.  The relationship between
	the two kinds of accessories is that the ItemOrderAccessory includes a
	Requested flag that allows the customer to select select, deselect, or
	select extra of an ItemOrderAccessory.
    *);
end MenuItemAccessory;

object IsStandard =  boolean;


(**
 * The next two objects define the restaurant inventory structure.
 **)
object FoodStuffsInventory extends SecureDB
    components: FoodStuffsItem*;
    operations: AddItem, DelItem, ChangeItem, FindItem;
    description: (*
	FoodStuffsInventory is the inventory of raw food ingredients, such as
	burger patties, buns etc.  This inventory contains a description of all
	stock on hand.  The equations specify that duplicate food stuffs items
	of the same name cannot be stored in the inventory.
    *);
end FoodStuffsInventory;

object FoodStuffsItem
    components: Name and Quantity and Units;
    description: (*
	A foods stuffs inventory item consisting of a name, quantity, and unit
	of measurement.  For example, if there are 500 hamburger patties on
	hand, then the inventory entry is:

		Name: "Patty"
		Quantity: 500
		Unit: "1/4 LB"

	Note that there is no size component here.  Size information must be
	put in the name of the item.  For example, there are small, large, and
	medium drink cups.  A sample small cup inventory entry is the
	following: 

		Name: "Small Drink Cup"
		Quantity: 450
		Unit: "8 oz"

	The medium and large cups would be entered similarly.
    *);
end FoodStuffsItem;

(*
 * The next two objects define the brief summary of the inventory contents,
 * output by the AddDelivery operation.
 *)
object InventorySummary
    components: InventoryItemCount*;
    description: (*
	A sorted list of inventory contents, by name and amount of stock on
	hand.
    *);
end InventorySummary;

object InventoryItemCount
    components: Name and Count and Units;
    description: (*
	The name of an inventory item and how much stock of it is on hand.  The
	stack on hand number is given in the appropriate units for each type of
	item.  E.g., the following is an InventoryItemCount for hamburger
	patties:
		Name: "Hamburger Patty"
		Count: 15
		Units: "Package of 25"
    *);
end InventoryItemCount;

object Count =  number;


(**
 * The next several defs are for atomic objects refereneced in FoodStuffsItem,
 * and elsewhere.
 **)
object Name =  string;
object Quantity =  number;
object Units =  string;
object Description =  string;
object Price =  number;


(**
 * The next several objects define the menu item breakdown list.
 **)
object MenuItemBreakdowns extends SecureDB
    components: MenuItemBreakdown*;
    description: (*
	The MenuItemsBreakdownList contains the complete breakdown for each
	food item on the menu.  Each breakdown describes exactly what raw food
	stuffs are need to prepare the menu item.
    *);
end MenuItemBreakdowns;

object MenuItemBreakdown
    components: Name and BasicParts and MenuItemAccessories;
    description: (*
	A MenuItemBreakdown describes the food stuffs components of
	customer-level food items on the menu .  For example, the breakdown for
	a plain hambuger is:

		Name: "Plain Hamburger"
		BasicParts: "patty", "bun"
		Price: 1.89
		Accessories: "Mayonaise", "Mustard", "Catsup", "Lettuce",
			"Tomato", "Pickles", "Onion", "Cheese", "Mushrooms"

	Note that there is similarity between a MenuItemBreakdown object and
	the MenuItem object defined above.  The difference is that a MenuItem
	is a description seen by the restaurant customer, whereas a
	MenuItemBreakdown is seen by the restaurant management and staff.  The
	most important specific difference between the two types of object
	that a MenuItem has a customer-oriented description, whereas a
	MenuItemBreakdown has a complete list of basic parts and extras.  In
	general, the customer-oriented description will not contain a full list
	of all parts.  For example, the customer-oriented description of a
	plain hamburger is "1/4 lb patty on a sesame seed bun", whereas the
	basic parts list of a plain hamburger MenuItemBreakdown is the list
	consisting of "patty" and "bun".
    *);
end MenuItemBreakdown;

object MenuItemBreakdownList
    components: MenuItemBreakdown*;
    description: (*
	A sorted list of breakdowns.  The postcond on ListMenuItemBreakdowns
	ensures sorted order.
    *);
end MenuItemBreakdownList;

object BasicParts
    components: FoodStuffsItem*;
    description: (*
	The basic parts of a menu item are those that are always included.  For
	example, the basic parts of a hamburger are the patty and bun.
    *);
end BasicParts;


(** The next several objects define database reports **)

object DBReport
    components: MenuItemList or InventoryList or IntervalInventoryReport;
    description: (*
	There are three types of reports that the system will generate.  A
	description of each is given below in the respective definitions.
    *);
end DBReport;

object MenuItemList
    components: MenuItemBreakdown*;
    description: (*
	A MenuItemList is a listing of all the menu items currently
	available on the food menu.  This list can be sorted alpahbetically or
	by menu section.
    *);
end MenuItemList;

object InventoryList
    components: FoodStuffsItem*;
    description: (*
	An InventoryList is a listing of all the raw food stuffs currently in
	the food stuffs inventory.  The listing is sorted alphabetically.
    *);
end InventoryList;

object IntervalInventoryReport
    components: Interval and AnnotatedMenuItemList and AnnotatedInventoryList;
    description: (*
	An IntervalInventoryReport is a listing of how many items sold in a
	given interval and how the inventory fluctuated during that time.  The
	possible intervals are daily, weekly, monthly, and yearly.
    *);
end IntervalInventoryReport;

object Interval
    description: (*
        The default interval for an IntervalInventoryReport is unspecified.
        Interval is specialized in the instances of IntervalInventoryReport
        defined below;
    *);
end;

object AnnotatedMenuItemList
    components: AnnotatedMenuItem*;
    description: (*
	The annotated menu item list indicates how many units of each menu item
	were sold in a given interval.  The interval is defined by the kind of
	report that the list appears in.
    *);
end AnnotatedMenuItemList;

object AnnotatedMenuItem
    components: Name and number;
    description: (*
	The Name is the name of a menu item (e.g., "Plain Hamburger") and the
	number is how many units of that menu item sold in a given interval.
    *);
end AnnotatedMenuItem;

object AnnotatedInventoryList
    components: AnnotatedInventoryItem*;
    description: (*
	The annotated inventory list indicates how many units of each raw
	foodstuffs item sold in a given interval.  The interval is defined by
	the kind of report that the list appears in.
    *);
end AnnotatedInventoryList;

object AnnotatedInventoryItem
    components: Name and NumberSold;
    description: (*
	The Name is the name of raw food stuffs item (e.g., "Hamburger Patty"
	and the number is how many units of that menu item sold in a given
	interval.
    *);
end AnnotatedInventoryItem;

object DailyInventoryReport extends IntervalInventoryReport
    where: Interval = Day;
    description: (*
	A DailyInventoryReport has inventory information for one day.
    *);
end DailyInventoryReport;

object WeeklyInventoryReport extends IntervalInventoryReport
    where: Interval = Week;
    description: (*
	A DailyInventoryReport has inventory information for one week.
    *);
end WeeklyInventoryReport;

object MonthlyInventoryReport extends IntervalInventoryReport
    where: Interval = Month;
    description: (*
	A MonthlyInventoryReport has inventory information for one month.
    *);
end MonthlyInventoryReport;

object YearlyInventoryReport extends IntervalInventoryReport
    where: Interval = Year;
    description: (*
	A DailyInventoryReport has inventory information for one day.
    *);
end YearlyInventoryReport;

object Day
    components: DayName and DayDate and Month and Year;
    description: (*
	A Day describes a single day in the calendar year, e.g., Wednesday 14
	October 1991.
    *);
end Day;

object DayName =  string;
object DayDate =  string;
object IntervalName =  string;
object DBSectionName =  string;
object MenuSectionName =  string;
object OldMenuSectionName =  string;
object NewMenuSectionName =  string;
object NumberSold =  integer;

object Week
    components: WeekName, Day*;
    description: (*
	One calendar week.
    *);
end Week;

object Month
    components: MonthName, YearNumber, Day*;
    description: (*
	One calendar month.
    *);
end Month;

object Year
    components: YearNumber, Month*;
    description: (*
	One calendar year.
    *);
end Year;

object WeekName =  string;
object MonthName =  string;
object YearNumber =  number;

(** Food Orders **)

object OrderSoFar
    components:  ItemOrder*;
    description: (*
	The OrderSoFar is the collection of all individual item orders input
	by the customer.  As the ordering operation is performed, the customer
	order is built up from the ordered items.
    *);
end OrderSoFar;

object ItemOrder
    components: ItemName and ItemAmount and ItemOrderAccessories
		and ItemUnitPrice and ItemAccessoriesPrice and ItemTotalPrice;
    description: (*
	An ItemOrder contains all of the information that describes what a
	customer has ordered, including the item name, amount, extras, unit
	price, extras price, and total price.
    *);
end ItemOrder;

object ItemName =  string;
object ItemAmount =  number;
object ItemUnitPrice =  number;
object ItemAccessoriesPrice =  number;
object ItemTotalPrice =  number;

object ItemOrderAccessories
    components: string*;
end ItemOrderAccessories;

object ItemOrderAccessory
    components: Name and IsStandard and Requested and ExtraRequested and Price;
    description: (*
	Each Accessory has a name, an indication as to whether it is standard,
	an indication as to whether it has been requested by the customer, an
	indication as to whether extra has been requested, and a price.  For
	example, here is the structure of a mayonaise accessory for a standard
	hamburger:
		Name: "Mayonaise"
		IsStandard: true
		Requested: true
		ExtraRequested: false
		Price: "no charge"
	This example indicates that Mayonaise is standard, it has been
	requested by the customer, no extra is requested, and there is no
	charge for it.  If an Accessory is standard, then it is normally
	included on a menu item unless the customer explicitly requests that it
	be removed.  The converse is true for non-standard a Accessory.  The
	ExtraRequested flag allows the customer to select extra of an
	Accessory, i.e., double it.  If ExtraRequested is true, then the Price
	is doubled.
    *);
end ItemOrderAccessory;

object Requested =  boolean;
object ExtraRequested =  boolean;


object CooksOrder
    components:  CooksOrderItem*;
    description: (*
	The list of items to be cooked for a customer order.  The cook receives
	this order electronically on a screen in the cooking area, as in Taco
	Bell and similar fast food restaurants.
    *);
end CooksOrder;

object CooksOrderItem
    components: Amount, ItemName, SpecialInstructions;
    description: (*
	
    *);
end CooksOrderItem;

object Amount =  number;
object SpecialInstructions =  string;

object CustomerReceipt
    components: ReceiptHeading, OrderSoFar*, GrandTotal, CallNumber;
    description: (*
	This is the hardcopy receipt the the customer receives after ordering
	is completed.
    *);
end CustomerReceipt;

object ReceiptHeading =  string;
object GrandTotal =  number;
object CallNumber =  number;


(**
 * The next four definitions are concrete object values that define the
 * standard sections of the food menu.  These constitute the default menu
 * values, and are changeable using the MaintainMenu operation defined below.
 **)

value StandardMenu:FoodMenu = [BurgerSection, DrinksSection, SidesSection]
    description: (*
	A StandardMenu represents the default menu structure as presently in
	place at the restaurant.
    *);
end StandardMenu;

value BurgerSection:MenuSection = [BurgerSectionName,
	PlainBurgerItem, DoubleBurgerItem, ChiliBurgerItem, SkinnyBurgerItem,
	KiddieBurgerItem]
    description: (*
	These are the defaults in the Drinks section of the standard menu.
    *);
end BurgerSection;

value DrinksSection:MenuSection = [DrinksSectionName,
	CokeItem, OrangeItem, SevenUpItem, DietCokeItem, DrinkSizes]
    description: (*
	These are the defaults in the Drinks section of the standard menu.
    *);
end DrinksSection;

value SidesSection:MeunSection = [SidesSectionName,
	FriesItem, OnionRingsItem, ApplePieItem, SidesSizes]
    description: (*
	These are the defaults in the Drinks section of the standard menu.
    *);
end SidesSection;

value BurgerSectionName = "Hamburgers";
value DrinksSectionName = "Drinks";
value SidesSectionName = "Sides";

object DrinkSizes
    components: Small and Medium and Large;
    description: (*
	The sizes for a drink.
    *);
end DrinkSizes;

object SidesSizes
    components: Small and Large;
    description: (*
	The sizes for a side order, except apple pie, which comes in only one
	size by default.
    *);
end SidesSizes;

value Small = "Small";
value Medium = "Medium";
value Large = "Large";

(**
 * The next five objects are the definitions of the standard burgers.
 **)
value PlainBurgerItem = [
	(* Name: *) "Plain Hamburger",
	(* Description: *) "1/4 LB patty on a sesame seed bun",
	(* Price: *) 1.89,
	(* Accessories: *) PlainBurgerAccessories
    ];

value DoubleBurgerItem = [
	"Double Hamburger",
	"Two 1/4 LB patties on a sesame seed bun",
	2.99];

value ChiliBurgerItem = [
	"Chiliburger",
	"1/4 LB patty with chili on a sesame seed bun",
	2.69];

value SkinnyBurgerItem = [
	"Skinnyburger",
	"Tofu patty and special sauce on a whole-wheat bun",
	2.09];

value KiddieBurgerItem = [
	"Kiddyburger",
	"1/6 LB patty on a small bun",
	1.69];

(**
 * The next five objects are the definitions of the standard burgers
 * accessories. 
 **)

value PlainBurgerAccessories = [
	(* Name		IsStandard	Price
	 =======================================  *)
	["Mayonaise", 	true, 		0	],
	["Mustard", 	false,		0	],
	["Catsup", 	false,		0	],
	["Relish",	true,		0	],
	["Lettuce", 	true,		0	],
	["Tomato", 	true,		0.10	],
	["Pickles", 	true,		0	],
	["Onion", 	true,		0	],
	["Cheese", 	false,		0.35	],
	["Mushrooms",	false,		0.50	]
    ];

value DoubleBurgerAccessories = [
	["Mayonaise", 	true, 		0	],
	["Mustard", 	false,		0	],
	["Catsup", 	false,		0	],
	["Relish",	true,		0	],
	["Lettuce", 	true,		0	],
	["Tomato", 	true,		0.10	],
	["Pickles", 	true,		0	],
	["Onion", 	true,		0	],
	["Cheese", 	false,		0.35	],
	["Mushrooms",	false,		0.50	]
    ];

value ChiliBurgerAccessories = [
	["Mayonaise", 	false, 		0	],
	["Mustard", 	false,		0	],
	["Catsup", 	false,		0	],
	["Relish",	false,		0	],
	["Lettuce", 	false,		0	],
	["Tomato", 	false,		0.10	],
	["Pickles", 	false,		0	],
	["Onion", 	true,		0	],
	["Cheese", 	false,		0.35	],
	["Mushrooms",	false,		0.50	]
    ];

value SkinnyBurgerAccessories = [
	["Mayonaise", 	false, 		0	],
	["Mustard", 	false,		0	],
	["Catsup", 	false,		0	],
	["Relish",	false,		0	],
	["Lettuce", 	true,		0	],
	["Tomato", 	true,		0.10	],
	["Pickles", 	true,		0	],
	["Onion", 	true,		0	],
	["Cheese", 	false,		0.35	],
	["Mushrooms",	false,		0.50	]
    ];

value KiddyBurgerAccessories = [
	["Mayonaise", 	true, 		0	],
	["Mustard", 	true,		0	],
	["Catsup", 	true,		0	],
	["Relish",	false,		0	],
	["Lettuce", 	true,		0	],
	["Tomato", 	true,		0.10	],
	["Pickles", 	true,		0	],
	["Onion", 	false,		0	],
	["Cheese", 	false,		0.35	],
	["Mushrooms",	false,		0.50	]
    ];


(**
 * The next four objects are the definitions of the standard drinks.
 **)

value CokeItem = "Coke";
value OrangeItem = "Orange";
value SevenUpItem = "SevenUp";
value DietCokeItem = "DietCoke";

(**
 * The next three objects are the definitions of the standard drinks.
 **)

value FriesItem = "Fries";
value OnionRingsItem = "Onion Rings";
value ApplePieItem = "Apple Pie";


(*
 * The next several objects are "organizational" collections used for inputs to
 * higher-level functions.
 *)
object CustomerSelections
    components: BurgerSelection or DrinkSelection or SidesSelection;
    description: (*
	This object is the collection of all possible selection inputs that
	user may provide during an order session.  It's an organizational input
	used in the high-level OrderFood operation.
    *);
end CustomerSelections;

object BurgerSelection
    components: PlainBurgerSelection, DoubleBurgerSelection,
	ChiliBurgerSelection, SkinnyBurgerSelection, KiddieBurgerSelection;
end BurgerSelection;

value PlainBurgerSelection = "Plain Burger";
value DoubleBurgerSelection = "Double Burger";
value ChiliBurgerSelection = "Chili Burger";
value SkinnyBurgerSelection = "Skinny Burger";
value KiddieBurgerSelection = "Kiddie Burger";

object DrinkSelection
    components: CokeSelection, OrangeSelection, SevenUpSelection,
	DietCokeSelection;
end DrinkSelection;

value CokeSelection =  "Coke";
value OrangeSelection = " Orange";
value SevenUpSelection = "Seven Up";
value DietCokeSelection = "Diet Coke";

object SidesSelection
    components: FriesSelection, OnionRingsSelection, ApplePieSelection;
end SidesSelection;

value FriesSelection =  "Fries";
value OnionRingsSelection = "Onion Rings";
value ApplePieSelection = "Apple Pie";


object DBUpdates
    components: MenuUpdates or InventoryUpdates or BreakdownUpdates;
    description: (*
	This object is the union of all possible DB update inputs that
	manager may provide during DB mainenance session.  It's an
	organizational input used in the high-level MaintainDB operation.
    *);
end DBUpdates;

object MenuUpdates
    components: MenuSectionName and Name and MenuItem;
    description: (*
	Union of possible menu updates.
    *);
end MenuUpdates;

object InventoryUpdates
    components: Name or FoodStuffsItem;
    description: (*
	Union of possible inventory item updates.
    *);
end InventoryUpdates;

object BreakdownUpdates
    components: Name or MenuItemBreakdown;
    description: (*
	Union of possible menu item breakdwon updates.
    *);
end BreakdownUpdates;




(**
 * OPERATIONS
 **)


(** Food Ordering **)

operation OrderFood
    inputs: cs:CustomerSelections, fm:FoodMenu;
    outputs: cr:CustomerReceipt, co:CooksOrder;
    precondition:
	(* Every item in the customer order is on the menu and in stock. *);
    description: (*
	Accumulate the individual customer entries and produce the food orders.
	The principal ordering constraint is that the customer-selected food
	item is on the input menu.  The menu will be updated as necessary
	during normal business to reflect immediate changes in inventory.
	E.g., if hamburger patties are consumed, then the Burger items will be
	deleted form the menu (deletion is specified by marking the item as
	``temporarily out of stock'' on the menu).  It should be noted that
	this ordering constraint requires human intervention to remove an item
	from the menu.  I.e., the manager must use the MaintainMenu function to
	perform the change.  Other alternatives for ordering constraints were
	considered, in particular, having the system automatically remove an
	item from the menu when the online inventory indicates that some
	comoponent of a MenuItem is out of stock.  This fully automatic
	operation was rejected on the grounds that the system may not have
	accurate information about the exact inventory on hand.  E.g., if the
	cook uses more of some FoodStuffs item then is required and fails to
	report the overuse to the system, the system will indicate that there
	is more of the FoodStuffs item than is actually available.  Instead of
	the fully automatic Menu update, the system will output a ``stock low''
	warning on the manager's console (see the MaintainMenu function).
    *);
end OrderFood;

operation OrderBurger
    inputs: MenuSection = BurgerSection, BurgerSelection, OrderSoFar;
    outputs: OrderSoFar;
    precondition: (*Selection is in the burger section of the menu and the
	selection is currently in stock.*);
    description: (*
	The OrderBurger operation accepts a customer order from the
	BurgerSection of the menu.  The BurgerSelection chooses one of the
	available items in the BurgerSection of the menu, and that item is
	added to the OrderSoFar currently being tallied.
    *);
end OrderBurger;

operation OrderDrink
    inputs: MenuSection = DrinksSection, DrinkSelection, OrderSoFar;
    outputs: OrderSoFar;
    description: (*
	The OrderDrinks operation accepts a customer order from the
	DrinksSection of the menu.  The DrinkSelection is added to the
	OrderSoFar currently being tallied.
    *);
end OrderDrink;

operation OrderSides
    inputs: MenuSection = SidesSection, SidesSelection, OrderSoFar;
    outputs: OrderSoFar;
    description: (*
	The OrderSides operation accepts a customer order from the SidesSection
	of the menu.  The SidesSelection is added to the OrderSoFar
	currently being tallied.
    *);
end OrderSides;

operation ComposeOrder
    inputs: OrderSoFar;
    outputs: CustomerReceipt, CooksOrder, DBUpdates;
    description: (*
	The ComposeOrder operation is invoked in repsonse to the customer
	indicating that the food order has been completed.  ComposeOrder takes
	the completed OrderSoFar and produces a final CustomerReceipt and
	CooksOrder.  The CustomerReceipt is presented to the customer at the
	table in paper form.  The CooksOrder is sent to the kitchen, where it
	appears on an electronic monitor.  The CooksOrders should be received
	in the kitchen in first-come, first-served order.  The last output is
	sent to the MaintainDB subsystem, to debit the inventory database by
	the appropriate amount of ingredients.
    *);
end ComposeOrder;


(** Database Management **)

operation MaintainDB
    inputs: RestaurantDB, DBUpdates;
    outputs: RestaurantDB, DBReport;
    description: (*
	The MaintainDB operation manages all components of the restaurant
	database.  MaintainDB performs password validation on the user, to
	ensure that only legitimate restaurant personnel may gain access to the
	databases.  The three main suboperations of MaintaiDB are described
	below.
    *);
end MaintainDB;

operation EnterPassword
    inputs: rdb: RestaurantDB, pwOld: Password, pwNew: Password;
    outputs: rdb': RestaurantDB;
    pre:     if rdb.pw != empty then rdb.pw = pwOld;
    post:     rdb'.pw = pwNew;
    description: (*
	Enter a password into the system.  This is the password that must be
	known by a user in order to gain access to the the restaurant database.
	The old password must also be known in order to change to a new one.
	When the system is initially brought up, the old password will by nil,
	so that only the a new one will be required when the system is
	initially started up.
    *);
end EnterPassword;

operation ValidateUser
    inputs: rdb: RestaurantDB, pw: Password;
    outputs: rdb': RestaurantDB;
    post:    
	if rdb.pw = pw then
	    rdb'.fm.av = true and
	    rdb'.fsi.av = true and
	    rdb'.bl.av = true
	else
	    rdb'.fm.av = false and
	    rdb'.fsi.av = false and
	    rdb'.bl.av = false;
    description: (*
	Validate a user by requiring the she know the current system password.
	The effect of user validation is recorded in the access validation
	flags in each of the major databases.  Each database requires its own
	access validation component, since each can be edited separately.
	Having the access validation only in the top-level RestaurantDB would
	require operations like AddMenuItem to input the entire RestaurantDB,
	in order to have access to the validation flag.
    *);
end ValidateUser;


(*
 * MaintainMenu and its suboperations.
 *)
operation MaintainMenu
    inputs:  fm:FoodMenu, MenuUpdates;
    outputs: FoodMenu, MenuItemList;
    pre:     fm.av = true;
    description: (*
	MaintainMenu allows new menu items to be added to the FoodMenu.  It
	also allows existing menu items to deleted, changed, or listed.  Menu
	sections can also be added, deleted, and changed.  As a precaution to
	massive data loss, only an empty menu section can be deleted.  I.e.,
	before a menu section can be deleted, all of its items must first be
	deleted indvidually.
    *);
end MaintainMenu;

operation AddMenuItem
    inputs: FoodMenu, MenuSectionName, MenuItem;
    outputs: FoodMenu;
    description: (*
	Add a new item to the Menu.
    *);
end AddMenuItem;

operation DelMenuItem
    inputs: FoodMenu, MenuSectionName, Name;
    outputs: FoodMenu;
    description: (*
	Delete an existing item from the Menu.
    *);
end DelMenuItem;

operation ChangeMenuItem
    inputs: FoodMenu, MenuSectionName, Name, MenuItem;
    outputs: FoodMenu;
    description: (*
	Change an existing item on the Menu.
    *);
end ChangeMenuItem;

operation ListMenuItems
    inputs: FoodMenu;
    outputs: FoodMenu;
    description: (*
	List all of the items currently in the menu.
    *);
end ListMenuItems;

operation AddSection
    inputs: FoodMenu, MenuSectionName;
    outputs: FoodMenu;
    description: (*
	Add a new (empty) section to the Menu.
    *);
end AddSection;

operation DelSection
    inputs: FoodMenu, MenuSectionName;
    outputs: FoodMenu;
    description: (*
	Delete an existing (empty) section from the Menu.
    *);
end DelSection;

operation ChangeSection
    inputs: FoodMenu, OldMenuSectionName, NewMenuSectionName;
    outputs: FoodMenu;
    description: (*
	Change (the name of) an existing section on the Menu.
    *);
end ChangeSection;


(*
 * MaintainInventory and its suboperations.
 *)
operation MaintainInventory
    inputs: InventoryUpdates, FoodStuffsInventory;
    outputs: FoodStuffsInventory, IntervalInventoryReport;
    description: (*
	MaintainInventory allows updates to the FoodStuffsInventory.  The
	AddDelivery suboperation is invoked when vendor deliveries arrive.
	DeleteSpoilage is typically invoked at the end of the business day to
	update the inventory based on how much food spoiled or was damaged
	during restaurant operations.  The Add, Del, and ChangeFoodStuffsItem
	operations provide the standard access to the inventory DB.  Finally,
	the ListInventory operation is used to produce an
	IntervalInventoryReport.
    *);
end MaintainInventory;

operation AddDelivery
    inputs: FoodStuffsInventory, InventoryList;
    outputs: FoodStuffsInventory, InventorySummary;
    description: (*
	Add a number of items to the inventory.  The intent is that this
	operation will be invoked when deliveries arrive.  The user will be
	prompted for each item successively and given a summary of the
	inventory after the inputs are made.
    *);
end AddDelivery;

operation DeleteSpoilage
    inputs: FoodStuffsInventory, FoodStuffsItem;
    outputs: FoodStuffsInventory;
    description: (*
	Delete a number of inventory items.
    *);
end DeleteSpoilage;

operation AddItem
    inputs: FoodStuffsInventory, FoodStuffsItem;
    outputs: FoodStuffsInventory;
    description: (*
	Add a single item to the inventory.
    *);
end AddItem;

operation DelItem
    inputs: FoodStuffsInventory, ItemName;
    outputs: FoodStuffsInventory;
    description: (*
	Delete a single item from the inventory.
    *);
end DelItem;

operation ChangeItem
    inputs: FoodStuffsInventory, Name, FoodStuffsItem;
    outputs: FoodStuffsInventory;
    description: (*
	Change an item in the inventory
    *);
end ChangeItem;

operation FindItem
    inputs: FoodStuffsInventory, ItemName;
    outputs: FoodStuffsItem;
    description: (*
	Find an inventory item by name.
    *);
end FindItem;

operation ListInventory
    inputs: FoodStuffsInventory;
    outputs: InventorySummary;
    description: (*
	Generate a summary list of the inventory contents.
    *);
end ListInventory;


(*
 * MaintainBreakdowns and its suboperations.
 *)
operation MaintainBreakdowns
    inputs: MenuItemBreakdowns, BreakdownUpdates;
    outputs: MenuItemBreakdowns;
    description: (*
	This operation maintains the MenuItemBreakdowns.  It has the
	standard suboperations to add, delete, change, and list database items.
    *);
end MaintainBreakdowns;

operation AddMenuItemBreakdown
    inputs: MenuItemBreakdowns, MenuItemBreakdown;
    outputs: MenuItemBreakdowns;
    description: (*
	Add a new breakdown to the list.
    *);
end AddMenuItemBreakdown;

operation DelMenuItemBreakdown
    inputs: MenuItemBreakdowns, Name;
    outputs: MenuItemBreakdowns;
    description: (*
	Delete an existing breakdown from the list.
    *);
end DelMenuItemBreakdown;

operation ChangeMenuItemBreakdown
    inputs: MenuItemBreakdowns, Name, MenuItemBreakdown;
    outputs: MenuItemBreakdowns;
    description: (*
	Change an existing breakdown in the list.
    *);
end ChangeMenuItemBreakdown;

operation ListMenuItemBreakdowns
    inputs: MenuItemBreakdowns;
    outputs: MenuItemBreakdownList;
    description: (*
	List out the breakdowns, sorted by name.
    *);
end ListMenuItemBreakdowns;


(*
 * The report generating operation.
 *)
operation GenerateReports
    inputs: RestaurantDB, DBSectionName = "Inventory", IntervalName = "Week";
    outputs: DBReport;
    description: (*
	Outputs a report for the given section of the database and the given
	interval.  The default is a weekly inventory report.
    *);
end GenerateReports;