Reference no: EM131759381

Software Verification Technology Assignment

Objectives - The purpose of the tasks below is to ensure that you can:

• read and write modelling scenarios in VDM/Overture;
• make appropriate modelling decisions;
• understand the role of specification (i.e. invariants, pre, post, etc.);
• understand the role of proof obligations;
• prove in Isabelle simple properties of interest about models;

1. Problem Scenario Description -

Dots-and-boxes is a pencil-and-paper game for i players of different colours who take turns within the spaces in an n × n grid. We illustrate the play on a 4 × 4 grid with two (blue, red) players (see grids in the picture below). Players take turns by joining exactly two dots with their corresponding colour in either a horizontal or vertical (but not diagonal) move (see middle grid). The game play must be fair: no player can play twice in a row; and whoever plays the fourth side of a box owns it, regardless of the surrounding colours (see right grid). Every box made leads to a mandatory extra move. Deciding when to make a box is optional (i.e. players can avoid it) and is part of possible winning strategies. The player with the higher number of owned boxes at the end wins.

The game requirements, move types, and winning strategies are described. You can also play it online at https://dotsandboxes.org. This game enjoys a number of interesting mathematical properties. For instance: there is a winning strategy for two players on grids with a "central box" (i.e. when n is even); the number of available moves is a function of the grid size and possible boxes; etc. The game is also useful to characterise (mathematically) interesting properties of interest, such as: who won?; what is the minimum/maximum number of moves possible to win?; what "types" of move are there?; etc. The game will be used it to ascertain your understanding of modelling and proof techniques.

2. Tasks Description

Using Overture and Isabelle, your task is to:

• create the board layout,
• define players valid-moves
• encode the game-play itself as a state-based model with operations

This VDM model does not need to be executable, but it might be easier to debug if you can "run" the game. A suggested state and top-level algorithm is given in Box on the next page. You can adjust it as you see fit. To complete the model for the suggested algorithm you will need to define data types, auxiliary functions and operations. Keep your model tidy; proper indentation and succinct comments are useful.

Next, you will need to translate the model to Isabelle in order to discharge proof obligations about satisfiability (i.e. operations contracts are feasible) and sanity checks (i.e. the game behaves as expected) for your model in Isabelle.

Hint: Decomposing the problem (as you see fit) and writing auxiliary functions for invariants and other properties help simplifying the solution by making it modular. Important issues to consider include (but are not limited to):

• types and invariants for board, position, player move, kinds of moves, etc;
• calculate the game stage (e.g. account for boxes, available moves, etc.);
• characterise moves so far, as well as those available to be taken;
• represent winning conditions and who won;
• specify the game state representation and invariants;
• write tests to convince yourself the model is suitable;
• prove satisfiability for operations involved;
• modelling decisions might affect how easy/hard proof work will be.

Aspects of the model to help you brainstorm solutions will be presented.

Task A - Write the game as a VDM-SL model

Purpose: Modelling decisions variety; documentation of design decisions.

Question: Provide a model to the problem scenario. This ought to include:

• constant, type, and invariant declarations;
• description of kinds of moves possible (see video @ goo.gl/oFhLRf);
• state invariant, pre and postconditions for operations;

You may also find useful to be modular, and use:

• (auxiliary) functions and operations;
• boolean-valued functions for (reusable) invariants, etc.

Explain and justify your choices with comments to inform the reader of your design decisions. Use VDM/Overture to typeset your model. Models do not need to be executable.

Answers using value enumeration (e.g. manually writing all possible moves will be tedious and error prone and) will not be considered. They can be useful for debugging but must not be your final answer.

Hint: Overture helps avoiding trivial mistakes and provide proof obligation statements to be proved in Isabelle (see Tasks C-D). It is useful to separate your model (and its invariants) per part.

1. Constants, types, auxiliary functions

2. Points of interest

3. Move types, and taken

4. pre/post conditions in auxiliary functions

5. State invariants

6. pre/post conditions in state operations

7. extended explicit operations are easier to follow

8. etc.

Task B - Translate your VDM model to Isabelle

Purpose: Understand interplay between VDM modelling and Isabelle proving.

Question: Translate your model from Task A into Isabelle and check it using Isabelle's value commands and/or auxiliary lemma statements.

Convince yourself (and write comments about why) the model makes sense. Have you built the model right? Have you built the right model?

Hint:

• nitpick can help debug your model;
• sledgehammer or "by auto" can help proving conjectures;
• If a proof is "too complicated", try simplifying your model;
• Isabelle does not enforce (implicit type/state) invariant/pre/post checks;
• Be systematic: translate it as if you had "a program" do it for you.

Task C - Discharge satisfiability proof obligations (POs) in Isabelle

Purpose: Understand modelling consequences in practice (through proof)

Question: Using Isabelle, state and prove: satisfiability proof obligations as given by Overture for majority of operations defined (i.e. moves_left, save, etc);

Revise and update your VDM model and Isabelle translation depending on results from (failed) proofs;

The more you prove (i.e. auxiliary functions and operations), errors can be compensated (i.e. if your model have 8 operations and you prove 6 POs; you can afford some mistakes in at least 2, since 4 correct proofs would suffice).

Hint:

• Look at proof exercises from lecturers;
• Write proof scripts, even if partial;
• Write a proof plan as comments if you fail to do it using Isabelle;
• If the model datatypes/invariants are chosen carefully, proofs commands like "by auto" or "by simp" should suffice after definition expansion.

Task D - State and prove sanity checks in Isabelle

Purpose: Understand the difference between verification and validation

Question: Having built a convincing model and proved its satisfiable, it is important to ensure that the model you have does what you want. That is the difference between verification (e.g. build the model right: it is satisfiable) and validation (e.g. build the right model: it behaves as expected).

Declare and prove in Isabelle at least two sanity checks of your choice. These can be (but are not limited to):

1. there can only be one winner;

2. available moves are within maximum board positions;

3. number of moves is fair (i.e. one move per player per round), etc.

As with satisfiability, if you prove more than 2, errors can be compensated.

Hint: You can use Isabelle's value command with concrete values on the chosen sanity check above, or use nitpick to find mistakes or misunderstandings quickly. It is similar to debugging in Overture.

Task E - Reflect on your learning experience

Purpose: Think about what you learned; reflect on outcomes; give feedback.

Question: Looking back at your design decisions, how did they affect the proofs involved? If anything, what would you have done differently and why?

Reflect and write on the modelling and proving Tasks A-D. What were your best/worst design decisions and why? How would you do it differently?

Write a brief personal account of the material you found hard to understand and how you overcame problems. What did you find difficult / interesting / worthwhile / fun in this course?

Hint:

Feedback on the material and style of presentation will also be much appreciated. This is a real chance to both say something technical and improve the course for future years!

Vacuous answers like "nothing was difficult" will only attract non-zero marks if other parts of the coursework were not superbly done.

Attachment:- Assignment File.rar