0657.424B: Advanced Software Engineering, 2001

Here is the project.zed source file for the 424 project: A Genealogy System. The due date is 2nd November 2001.

The 524 project is also now available. If you haven't yet received it (and you are taking 524), email me and I'll make sure you get the documentation. The due date is 16th November 2001.

A major theme of the course is how precise specifications (we use the Z formal specification language) can help you to produce better software cost-effectively.

We cover formal specification and show how it can be used to specify systems at a high level of abstraction ("what it should do, rather than how it should do it"). The writing of such specifications typically reduces ambiguity, allows precise reasoning about the system, and leads to system designs that are simpler yet more general.

We also show how these more precise specifications can have benefits on other more traditional areas of software development, such as requirements capture, unit testing, inspections, and code verification (concentrating on the use of assertions).

We are using the Z/EVES system in this course. It supports typechecking and theorem proving for the Z specification language, and is probably the most highly automated Z theorem prover currently available. You will need this z-eves.sty file in your current directory to typeset Z specifications. Do these commands from a shell window:

    latex spec.zed
    xdvi spec.dvi               (to view it)
    dvips -f spec.dvi | lpr     (to print it)

Contact me is you want to (try to!) install z-eves under linux on your own system.

The course contains six modules, each two weeks long. Here are the titles of the modules, plus a few useful online resources for them---which I'm adding to as we go.

Module 1: "Computers that Kill"

An overview of the IEC 1508 draft standard is available online.

For Ethics, look at WWW Ethics Centre for Engineering and Science.

Does it pay to improve your software process? Here is one study that suggests it does.

In his paper 'No Silver Bullet', Fred Brooks argues that software is intrinsically difficult, and no new technology can lead to order-of-magnitude reductions in software cost (unlike hardware costs). Brad Cox disagrees, and says there is a silver bullet, but it requires a paradigm xshift, not just a new technology. What do you think?

Module 2: "What does it do? Reading Z specifications"

You can access Jaza in the G-basement labs (or download it---the binary release is easiest) and use it to evaluate toolkit expressions. For example:

    tar xzvf jaza_linux.tgz
    cd jaza
    ./jaza
    JAZA> eval \power \{ 1,2 \}
    \{\{\}, \{1\}, \{1, 2\}, \{2\}\}

Here is documentation for Z/EVES, most useful first:

• Reference Card (included in the module 2 handout)
• Z/EVES 2.0 User's Guide (71 pages). The first 18 pages are the most useful for this course, but some of Section 3 (pages 19-34) are also relevant.
• Z/EVES Reference Manual (74 pages). Contains a detailed description of each Z/LaTeX construct and all the commands that Z/EVES provides.
• Z/EVES Mathematical Toolkit (91 pages). A reference manual that describes every theorem about every Z operator (useful if you are trying to do proofs with Z/EVES).
• Software Manual for Unix Z/EVES Version 2.1 (15 pages). Mostly about installation of Z/EVES.
• Software Manual for Windows Z/EVES Version 2.1 (16 pages). Mostly about installation of Z/EVES.

Lots of information about formal methods, especially Z, is available from the Oxford formal methods archive.

The answers to Test One are here.

Note that I made a series of (textually) small but vital mistakes in question 3, parts (d), (e) and (f). In (d) and (e) there should not have been any primes on Init. As it stands, both (d) and (e) are not even syntactically well-formed (since the declarations required for Init' to be well-formed as a predicate have not been made, i.e. we have only left and right and not left' and right' declared).

In (f) there should have been a \Delta before the Editor. Again, as it stands this is not even a well-formed predicate since not all the declarations required have been made if we leave out the \Delta.

So, apologies for that. The answers have assumed the correct form of the questions, so take a look. When marking this I'll take these mistakes into account, of course! I'll go over both correct and incorrect questions in the lectures.

Module 3: "Test, Test and Test Again"

Here are some simple Z specifications for you to use when you experiment with animation/testing:

• counter.zed;
• blocks.zed

The assignment for this module requires you to animate and test a specification.

Here are the files that you will need in order to do the assignment:

• grades.zed which contains the specification of the grades system;
• gsys.tar, a 'tar' file which contains the six implementations (five of them faulty) for you to try your testset on;
• run_tests, a script to help you organise you test runs;
• part3.zed, to help you make a start on your TTF presentation.

Module 4: "What do I want it to do? Writing Z specifications"

Here is some discussion on how inspection is widely-used (or not) in industry and factors that influence this.

Module 5: "Reactive Systems? In Z?"

Miscellaneous References

[From SVRC Update 6, Oct 1999] The Data & Analysis Center for Software (DACS) is an excellent starting point for information on all facets of software engineering. DACS also make their technical reports available on-line in multiple formats. An example of their coverage is in the area of Cost Estimation: "Techniques, methods, and tools for planning, estimating, and monitoring the cost, budget, or schedule of a software project. Included in this discussion are Function Point and Lines-of-Code cost estimation techniques." See: here and here.