Answer Happy

1. Introduction This coursework requires you to develop a B specification of a version of the Battleships board game. This system is to be developed using the tools Atelier B&Pro In addition prove implementation fragments are comect using Hoare Logic Bath is a strategy type guessing game for two players. It is played using te grids, one for each player. The game starts by each player placing the warships of their feet on squares in their own grid. The locations of the fleets are concealed from the other player Players take atemate tums "shooting at the other player's ships in an attempt to sink them The aim of the game is to win by destroying your opponents fleet of ships before shehe destroy your feet of ships See tus dawBettens in 10 9 K 7 5 4 3 2 t M Figure 1. Example of a Player's Battleships Board with 3 ships in positions (1.6) (6.5) (8.3) Player 2 shoots at For example, Player 1 has their feet positioned as in Figure 1, then square (8.3) then shehe scores a hand sinks the ship in that ship in square (8.3) is removed from the board, leaving Player 1 with at the 2 ships in squares (16) & (88) on Player 2's next tum shehe "shoot at square (44) then it is miss and has no effect on Player T's shipe The winner of the game is the Player who sinks all of the other Player's ships before all of their own ships are sun 1.1 The Battleships Game Constraints and Requirements For the purposes of this coursework, the Battleships game used is a simplified version of the normal game A grid size of 10 x 10 squares with the grid square (68) representing the square t column 6 & now Each player has 3 warships in the feet . Each warship occupies a single grid square on the grid The warships must be on different grid squares, Le at most 1 warship per square SENG001Weed Deered Coursework 2 1.2 Playing the Battleships Game The Batteships game is playas 1. The game starts by each player placing their 3 ships on their own grid, each player's ships in different grid squares 2. Player 1 has the first 3 Player 1 shoots at Player 2's ships, by selecting a target square on Player 2 gid there is a ship in the target square it is a he & the ship is deleted from Player 2 otherwise it is a miss and there is no change to Player 2's feet 4th Player 2 5 Player 2 shoots at Player T's ships, by selecting a target square on Player T's grd Registering it or miss, as above 6. The players continue to take turns un all of one player's ships have been sunkat this point the player who has at least 1 ship is the winner 2. The Battleships Game B Specification 2.1 Specification Components Your B specification should include the following elements (a) Sets and Constants Any sets and constants that are required to define the data and state of the Ba game system, and their properties (b) System State The state variables required to represent the data for the Battleships game system Including the state invariant and nation (c) Operations The four Batleships game operations are
(e) Operations The four Battleships game operations are report <--Blayer DeployFleet( ships ) Player 1 places their 3 ships on their own grid, by recording their positions on the grid if the ships are all placed in valid and position then the operation reports su otherwise it reports an eror message indicating what the error was report <-- Bayer DeployFleet( ships ) Player 2 places their 3 ships on their own grid, sinary to the Player 1 operation report <-- Playeri_Shootat target Player 1 shoots at the target square on Player 2's grid. If there is a sho square the ship is deleted and the operation reports at the hit sh in Player 2's foot the game is over and reports that the feet a otherwise there is no ship in the target square the operation reports as the target square is not in the grid it reports an error message 65ENG001W Refered Course 2 report <--Player2_Shootst target) Player 2 shoots at the target square on Player T's grid Operation is similar to the Player 1 operation Note that all operation must output the outcome of an operation, le succes the reason why it failed with an appropriate error message d) Enquiry Operations You must also specify the following enquiry operations, that all output information about the state of the game shipsquares - Locationships (player) Outputs the location of all the ships left in the player's feet shipsCount <-- Shipsteft(player) Outputs the number of ships let in the player's feet shatCount -- Shotstaken(player) target last one Outputs the number of shots taken by the player report - Gaver Outputs a message reporting the game is over. Le one of the players has won 2.2 General Requirements The specification should use the appropriate features to define the data & operations in any machines that you define. The overall structure of the specification can be ther A single B machine that contains all of the state information and operations, etc • A collection of machines that together contain all of the state information and operations, etc. The appropriate 8 structuring features must be used to combine the collection of B machines You should only submit one specification either a single B machine or a collection of S machines, but not both. More marks are available for a multi-machine specification than a single machine specification The specification must be syntactically & type comect, as checked by using the Atelier tool The specification must be animated by Prol. That is it must initialise comectly & all operations can be animated successfully & can be used to place ships and shoot at ship ENG001W RefCourse 2 3. Hoare Logic 10
3. Hoare Logic A simple strategy for choosing targets is to scan the opponent's map row by now, as implemented in the program P given below (modelling only coordinates not map cont *** P wide x 10 y 10 do 10th x end ****1 X+0 y*y*1 end (4) Show that the formula 10 & yox10 is a loop invariant for the while loop in P (b) Show that satses the Hoarele x=10&&y=101 by determining the intermediate assertions for each point i invariant from part() 4. Blackboard Submission The following 5 components are to be submited via Blackboard (1) The Structure Diagram of the Battleships Game machines) You must also include as a note with the diagrama "Plain English explanation of the "state invariants of the system Examples of Structure Diagrams can be found in the lecture notes and in the tutorial exercises. SENGODTWD Coursework 2 SUBMIT: 1 "PDF" gram using the loop [10 MARKS] (2) The Specification of the Battleships Game System, ie, the abstract machine SUBMIT B machines) a plain ASCII Text is "mch 150 MARKS] 140 (3) Examples of successfully using the 2B tools Alser Band Pro For Atelier a single screen shot showing Aller's mainwindow with the successful type checking of all machines in the specification, the specification box with the green TC circle For Proß: a Graph representation of a complete Pro Animation Session history. Using Proß perform an animation session that shows a game being played from start to finish, that includes shots that are hits and misses View this Animation Session a a DOT graph and then save SUBMIT (4) The Hoare Logic proofs 1 Atelier screen shot in either "jpg" or "jpeg" format 1 Pro animation graph "dor e as is (DO NOT open using Word) SUBMIT Hore Logic document as a POF [10 MARKS DeMARKS]