Formal Software Development

Spring Semester 2008

Course Organisation/Dates

Course Aims





Resource Materials

WeekFiles for viewing/downloadSourcesCommentSamples
1 (is stable for 2008) Practical Class 1 lab1.pdf lab1Dispenser.mch Introduction to the B-Toolkit lab1MyDispensersoln.mch solution
2 (is stable but we will jump to wk3 in 2008. this lab is fyi and can be used as an extra exercise) Practical Class 2 lab2.pdf None Introduction to Relations Lab2Register.mch solution
3 You should first read the overall lab sheet so that you get an idea of the overall picture of what the machine will look like overall. The lab sheet contains the overall interface description of the system.

Practical Class 3 (for wk3 of 2008 course) lab3.pdf

Walkthrough of lab 3walkthrough lab 3 pdf

The following is just an example of a function to demonstrate some of the ideas we covered in the last lecture. You should start the lab by animating this machine. wk2Function.mch

If you want to do the lab by yourselves then use the following: lab3.mch

If you want to do the lab by using the walkthrough to guide you then you'll need the following two files: CheckoutSource.mch lab3Fragment.txt

The following file is an example solution to the version created during the walkthrough CheckoutSoln2.mch

Developing a machine with sequences and a complex invariant None
4 Walkthrough lab (This file was created using the automatic document generator in the B-Toolkit) walkthroughwk4.doc.pdf

Practical Class 4 lab4.pdf

This first machine is used to help you get used to the proof obligation generator. wk4Paper_debt.mch

The next two machines accompany the lab sheet ProjectsSource.mch


Introduction to Proof Obligations Lab4Project.mch Solution

Lab4Regsoln.mch Solution

5 There is no walkthrough class this week. The lab is based on this practical and the coursework handed out.

Practical Class 5 lab7 pdf

Files for Question 1 LibData.mch


Files for Question 2 Examination.mch


Introduction to structuring Library.mch

6 (not yet stable for 2008) Practical Class 6 lab4.pdf SmallSet.mch


Introduction to Refinement SmallSetR.ref Solution

TeamR2.ref Solution

8 (done on 05/03/08)

Practical Class week 8 lab 7

Walkthrough in week 8 showing more complex loop invariant walkthroughwk8



These are the files for the walkthrough session WordTracker.mch




Implementations lab8 solution document
9 (done on 12/03/08) We only have one lab sheet today. (I am preparing the second coursework.This is not quite ready yet.)

Lab 9 lab 9 doc pdf

Lab sources Filter.mch



Implementations and Library machines in more detail None
10 We do have a walkthrough this week wk10 pdf

The following is an example of how to go about doing a review of a B specification. There is an exmaple specification and a review checklist wk10 pdflab10review

wk10 pdfB review guidelines

Walkthrough sources Clock.mch


The following is a skeleton of the one you need to build. LightActionsTemplate.mch

Lab sources TopLevel.mch





Linking B to software engineering The following is a sample solution to the walkthrough LevelCrossingSystem.mch

Substitute this machine for the LightActions machine. LightOrig.mch

You can save the B files into your home directory using Internet Explorer. Click the right mouse button on one of the links, and choose 'Save Target As...'. Find an appropriate subdirectory of your home directory to save the files into. But before you click the 'Save' button, make sure you change the box labelled 'Save as type:' to 'All files' rather than 'Text document'. This stops Internet Explorer from adding a '.txt' extension to the file name when it saves it.

Lab session instructions

There is one main CASE tool two that we shall be using in lab sessions which is the B-Toolkit developed by B Core Limited.

Editing files

The files that you will be editing are text files in UNIX format. This means that if you attempt to edit them in Windows Notepad, the text will all appear on one very long line. It will be very difficult to follow what is going on. If you put the line breaks in using Notepad, then the B-Toolkit will not complain. You can do this when you want to start writing a B specification outside the toolkit. However, once you have introduced it to the toolkit you will need to edit it within the toolkit environment. The Btoolkit is a configuration management tool as well as a tool which supports formal development and therefore if you try to by pass the configuration management you will get in a mess.

Go to the University of Surrey's Home Page Hosted by Computing @ Surrey This page is maintained by Helen Treharne.