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 B tools Atelier B & ProB. In addition, prove implementation fragments are correct using Hoare Logic. Battleships is a strategy type guessing game for two players. It is played using two 10 x 10 grids, one for each player. The game starts by each player placing the warships of their fleet on squares in their own grid. The locations of the fleets are concealed from the other player. Players take alternate turns "shooting" at the other player's ships in an attempt to sink them. The aim of the game is to win by destroying your opponent's fleet of ships before she/he destroys your fleet of ships. See https://en.wikipedia.org/wiki/Battleship_(game XXXXXXXXXX___ 7 6 ___ XXXXXXXXXX___ XXXXXXXXXX 9 10 Figure 1. Example of a Player's Battleships Board with 3 ships in positions (1,6), (6,8), (8,3) For example, if Player 1 has their fleet positioned as in Figure 1, then if Player 2 “shoots” at square (8,3), then she/he scores a “hit” and sinks the ship in that position. This means the ship in square (8,3) is removed from the board, leaving Player 1 with just the 2 ships in squares (1,6) & (6,8). If on Player 2's next turn she/he “shoots” at square (4,4) then it is a “miss” and has no effect on Player 1's ships. The winner of the game is the Player who sinks all of the other Player's ships before all of their own ships are sunk. 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 (6,8) representing the square at column 6 & row 8. • Each player has 3 warships in their fleet. • Each warship occupies a single grid square on the grid. • The warships must be on different grid squares, i.e. at most 1 warship per square. 6SENG001W Referred/Deferred Coursework 2 4 [14/6/2022] 1.2 Playing the Battleships Game The Battleships game is played as follows: 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 turn. 3. Player 1 shoots at Player 2's ships, by selecting a target square on Player 2's grid. If there is a ship in the target square it is a hit & the ship is deleted from Player 2's fleet, otherwise it is a miss and there is no change to Player 2's fleet. 4. It is then Player 2's turn. 5. Player 2 shoots at Player 1's ships, by selecting a target square on Player 1's grid. Registering a hit or miss, as above. 6. The players continue to take turns until all of one player's ships have been sunk, at this point the player who has at least 1 ship left 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 Battleships 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 initialisation. (c) Operations The four Battleships game operations are: report <-- Player1_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 grid positions then the operation reports success, otherwise it reports an error message indicating what the error was. report <-- Player2_DeployFleet( ships ) Player 2 places their 3 ships on their own grid, similarly to the Player 1 operation. report <-- Player1_ShootsAt( target ) Player 1 shoots at the target square on Player 2's grid. If there is a ship in the target square the ship is deleted and the operation reports a hit; if the hit ship is the last one in Player 2's fleet the game is over and it reports that the fleet is sunk you win; otherwise if there is no ship in the target square the operation reports a miss. If the target square is not in the grid it reports an error message. 6SENG001W Referred/Deferred Coursework 2 5 [14/6/2022] report <-- Player2_ShootsAt( target ) Player 2 shoots at the target square on Player 1's grid. Operation is similar to the Player 1 operation. Note that all operations must output the outcome of an operation, i.e. successful or if it fails, 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 <-- LocationOfShips( player ) Outputs the location of all the ships left in the player's fleet. shipsCount <-- ShipsLeft( player ) Outputs the number of ships left in the player's fleet. shotCount <-- ShotsTaken( player ) Outputs the number of shots taken by the player. report <-- GameOver Outputs a message reporting if the game is over, i.e. one of the players has won. 2.2 General Requirements The B specification should use the appropriate features to define the data & operations in any machines that you define. The overall structure of the B specification can be either: • A single B machine that contains all of the state information and operations, etc. • A collection of B machines that together contain all of the state information and operations, etc. The appropriate B 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 B machines, but not both. More marks are available for a multi-machine specification than a single machine specification. The specification must be syntactically & type correct, as checked by using the Atelier B tool. The specification must be animated by ProB. That is it must initialise correctly & all operations can be animated successfully & can be used to place ships and shoot at ships. 6SENG001W Referred/Deferred Coursework 2 6 [14/6/2022] 3. Hoare Logic A simple strategy for choosing targets is to scan the opponent's map row by row, as implemented in the program P given below (modelling only coordinates, not map contents): (a) Show that the formula x<=10 && y<=10 is a loop invariant for the while loop in P. (b) Show that P satisfies the Hoare triple [true] P [x = 10 && y = 10] by determining the intermediate assertions for each point in the program, using the loop invariant from part (a).