CS266 - Formal Specification and VerificationHW #6 -- Winter 2009More ASLAN Specifications and Proof ObligationsDue: Thursday 19 FEB 09Part I -Exercise to Complete Existing SpecificationConsider the following problem:Afarmer has to carry a goat, a cabbage, and a wolf from one side of the rivertothe other.Hehas aboat to do so, but the boat cannot carry more than three items, whether man, goat, cabbage, or wolf. If heleavesthe goat and the cabbage on the same side of the riverorinthe boat without being present, then thegoat will eat the cabbage. Similarly,the wolf will eat the goat if the farmer is not present.An incomplete ASLAN specification for the problem is presented below. You are to fill in the invari-ant and the necessary pre and post conditions for the single transition Transport. Your invariant shouldexpress the critical constraints of the problem. Youare not to solvethe problem. Therefore, your entryassertion only need express the obvious requirements, such as boat capacity.What you aretoturnintomefor this question is the listings of the .out file corresponding to thequestion.SPECIFICATION BoatLEVEL Top_LevelTYPERiver_Bank IS (East, West),Occupant_Type IS (Farmer,Goat, Cabbage, Wolf),Occupant_Set IS SET OF Occupant_TypeVA RIABLELocation(Occupant_Type): River_Bank,Boat_Location: River_BankCONSTANTCardinality(Occupant_Set): Integer/* Indicates the number of elements in the set */INITIALFORALL o:Occupant_Type (Location(o) = East)&Boat_Location = EastINVARIANT*** FILL THIS IN ***TRANSITION Transport(Passengers:Occupant_Set)/* This transition movespassengers from one side of the rivertothe other in the boat */ENTRY*** FILL THIS IN ***EXIT*** FILL THIS IN ***END Top_LevelEND Boat-2-Part II -Checking the Correctness of Aslan Theorem Generation1) You are to use the Aslan processor to generate the conjectures for the top-levelspecification of thesecure terminal example (using file secTLS) and to generate the conjectures for the second-levelspecifica-tion of the secure terminal example (using file sec2LS).2) For the Initial Conditions, Connect_To, and Send_Data conjectures for the top levelspecification youare to mark the constituent parts using the notation presented on page 24 of the Aslan User’sManual.Also, indicate if anyofthe conjectures generated are incorrect.3) For the Initial Conditions, Connect_To(for both mapping Connect_To_High and mapping Con-nect_To_Low), and Review_Data (for the mapping to Accept ONLY)conjectures for the second levelspeci-fication you are to mark the constituent parts using the notation presented on pages 25-27 of the AslanUser’sManual.Again, indicate if anyofthe conjectures generated are incorrect.DO NOTprint out all of the conjectures only those parts that you aregoing to mark.The Aslan processor output for the secTLS specification is 23 pages and for the sec2LS specificationis 65