This assignment is done through object-z specification language. No need to provide a LaTeX file just write out in pencil what needs to be done!

3 Type system We introduce the basic types [Description, Coordinate], as well as the composite type Point Coordinate x Coordinate We also introduce an enumerated type Message which will assume values that pond to error messages 4 Your assignment Consider a map which can be annotated with locations. Upon instantiation, a map object contains no annotations. A location is a pair of description and its corresponding point Even though descriptions are unique, locations may share a point on the map Define class Map to support the following operations: AddLocationOK: Adds a new location on the map DeleteLocationOK: Deletes an existing location from the map ModifyLocationoK: For a given description, it modifies its corresponding point on a map. FindLocationOK: For a given description, it provides its ma ing point on the You will also need to provide appropriate error operations, thus combining the definitions above to produce robust specifications for the following interface: AddLocation . DeleteLocation ModifyLocation FindLocation Subclassify Map to introduce class Map2 that behaves exactly like Map, while keeping track of the total number locations. 5 What to submit Please follow the instructions carefully: 1. Use LTX(a template is provided) to prepare the formal specification for classes Map and Map2 in Object-Z in a single file, map.tex, and produce a single pdf file called map.pdf 3 Type system We introduce the basic types [Description, Coordinate], as well as the composite type Point Coordinate x Coordinate We also introduce an enumerated type Message which will assume values that pond to error messages 4 Your assignment Consider a map which can be annotated with locations. Upon instantiation, a map object contains no annotations. A location is a pair of description and its corresponding point Even though descriptions are unique, locations may share a point on the map Define class Map to support the following operations: AddLocationOK: Adds a new location on the map DeleteLocationOK: Deletes an existing location from the map ModifyLocationoK: For a given description, it modifies its corresponding point on a map. FindLocationOK: For a given description, it provides its ma ing point on the You will also need to provide appropriate error operations, thus combining the definitions above to produce robust specifications for the following interface: AddLocation . DeleteLocation ModifyLocation FindLocation Subclassify Map to introduce class Map2 that behaves exactly like Map, while keeping track of the total number locations. 5 What to submit Please follow the instructions carefully: 1. Use LTX(a template is provided) to prepare the formal specification for classes Map and Map2 in Object-Z in a single file, map.tex, and produce a single pdf file called map.pdf