Description for Modelling and Reasoning

Task: Description for Modelling and Reasoning

This is a task description for the Modelling and Reasoning topic. It should be read in conjunction with the overall Project and Report (  specification.

Edit 16/03/2022: Step 1 has been simplified and Step 2 (updating  check_letter ) moved to the end.

Edit 20/03/2022: Initial versions of the model had lowercase words in the lists, which means that all guesses have to be lowercase as well. This was changed in later versions. Capitalised versions can be found here if you prefer them: allowed.vdmsl ( ( answers.vdmsl ( ( (just overwrite the files).

Edit 19/04/2022: Added instruction to add IO.vdmsl library.

Edit 28/04/2022: Removed incorrect recursive call to call to  test_check_letter within test_check_letter .


You have been asked by the New York Times to complete the VDM model of Wordle so that they can understand how it works (since they purchased it for an undisclosed seven-figure sum at the end of January), and to extend. You should begin with the basic model completed during the practical sessions. A clear version of the solution is available as: ( ( .


There are a variety of improvements that will make the model more useful to our clients at the New York Times, particularly given the first version covers only the basic functionality.

1. Since it may have been while, run the model and try the  check_letter function, and check_guess and  guess operations with various values. To do this you can:

Press Run > Start Debugging and then type in the console, e.g.  print check_letter('C', 1, "CHECK") or  print check_guess(w1, "HEALS") .

Click the Launch button above a definition and enter arguments when prompted. Note: tests might not all pass at this stage.

If you have not seen the specification before, it is worth going back through from

Modelling Wordle Part 1. ( For technical issues, the Frequently Asked Questions (FAQ) ( will be updated if comong problems are found.

2. Consolidate your tests for the current operations and functions in one place so they can be run repeatedly. To do this:

Create a second file called  test.vdmsl and add an operation called  test_check_letter: () ==> () that combines your test cases into one operation. This takes no parameters and returns no value.

Right-click on a .vdmsl file (e.g., test.vdmsl) there should be a “VDM” entry at the bottom. Under that menu select Add VDM Library and check IO at the top, and click Okay (this adds IO.vdmsl ( (  to the directory).

It should use the  IO`printf operation to print information to the console about expected and actual values for each test.

IO`printf takes a string containing  %s placeholders and a sequence of values, e.g.

IO`printf("Expected: <GREEN>, actual: %s", [check_letter(c1, p1, word1)]) .

You can use a values section to create named constants that can be used in multiple tests (as was done with  w1 ,  w2 etc. originally).

3. Create similar tests for the  check_guess and  guess operations.

4. Wordle has a "Hard mode" with the following definition: "Any revealed hints must be used in subsequent guesses." This rule further constrains what strings a user can guess with. Include this as a new operation called  hard_guess based on the  guess operation that meets this requirement.

Hint: the pre-condition should constrain what guesses the player can make, the operation body will not change.

Extend  test.vdmsl with  test_check_letter

5. Create an operation  hint: () ==> Hint that gives the user an appropriate hint given the state of the game. Define a  Hint type using an appropriate basic type (e.g., a  char ). Consider any pre-conditions required as well as defining the operation body. Document any assumptions you make in interpreting this requirement in your report.

6. You should discover that the naive implementation of the  check_guess combined with check_letter does not produce correct results in all situtations, i.e. where there are repeated letters. Improve the  check_letter function so that is passes the tests. Improve the specification to fix this issue.

Hint: the colour of a letter is conditional on the number of other occurrences of the letter in the word.

There are several ways to achieve this. For example,  check_letter could be updated to take in sufficient additional information to provide the correct colour, or the body of check_guess could be changed to directly compute the clues without  check_letter .


There are several ways the specification can be extended:

Additional invariants. Consider any further constraints on the  state Game covering the relationship between  gstate and  guesses and add to the invariant definition. Continutous gameplay.

The model does not directly provide information on what the state of the game is. Add an operation that prints out the number of guesses remaining, or the final state of the game, as appropriate.

The secret word is hard coded in the  init clause of the state definition and the game only runs once. Add a  reset operation and . Consider pre-conditions

Expansions. There are a variaety of Wordle clones building on the idea. Duplicate and rename your  wordle.vdmsl when trying these to preserve the main tasks:

Dordle:    (

Quordle:    (

Octordle:    (

What to Include in Your Report

The What Was Done and How section of your report could include: A description of the features of the model that were added.

A description of additional or changed data types and any invariants.

A description of key functionality added or updated, including pre- and post-conditions.

A description of how the model realises the requirements and any assumptions made in interpreting natural-language requirements.

Details of how the model was tested.

Model snippets of elements such as types, state, functions, operations and pre- and post- conditions to support the descriptions.

It is your decision as to what to include to demonstrate the work you have done.

Timetable and Deadlines

Practical sessions to support this task are Mondays 14:30 to 16:30 in 3.018. Remember to submit your report and artefact by Monday 16th May at 15:00.