Apologies for momentarily bringing this thread back
to life, but I've finally received approval from my MD
to post the following data. Apologies for
the delay.
 - Rod Chapman, Praxis

-----------------------

Here are some data relating to "formal methods" training on one of our
current, principal, software engineering projects.

There have actually been two project phases - a "specification" phase
and an "implementation" phase.

The first phase relates to work carried out to elicit requirements and
produce a first reviewed baseline of the formal specification and
architecture of the system.

The second "implementation" phase refers to the building of the actual
operational software, including changes, maintenance and updates to the
specification, which continues as you'd expect.  The formal specifications
are actively maintained to this day.

Specification Phase
-------------------

The team's average size was 14.  Of these, 3 Praxis staff came with
significant Z experience.

5 more Praxis full-time staff and 6 customer domain experts were
training to read and write Z during this part of the project.

Of the original 14 members of the specification team, I can identify
three that have PhD level qualifications.
One is in "Computer Science", one in Chemistry (OK...that's Anthony
Hall), and one in Paleobotany.

More recently, the on-going specification maintenance team has been
augmented by 2 sub-contractors who came with some Z skills. 

Implementation Phase
--------------------

Three particular training courses have been taught to support this
part of the project:
+ Z Readers Course
+ Introductory SPARK
+ Advanced SPARK

The principal skills needed are the ability to read Z and derive
code (which is almost all SPARK) and/or test cases.

These data are for all the people that have ever worked on the
implementation project, so do not reflect the actual size of the
current team.

The numbers for each course, broken down by staff categories, are
as follows

Z Readers Course:          
  + Praxis staff                          31
  + Client staff                          10
  + Contractors and partner company staff 47

Introductory SPARK:   
  + Praxis staff                          20
  + Client staff                          12
  + Contractors and partner company staff 25

Advanced SPARK:  
  + Praxis staff                          9
  + Client staff                          4
  + Contractors and partner company staff 3

Observations
------------

1) It seems we can teach customers and domain-experts to
   read and write Z effectively.  In particular, these
   people have made a significant contribution to the specification
   production and maintenance. The Z-writing learning curve is
   non-trivial though - probably 3 months after initial training
   before real Z-writing fluency is achieved. The Z-reading learning
   curve is much shorter and shallower.

2) We have been able to take on a significant number of contractors
   and train them to both read Z and produce SPARK.

We hope to publish these data (and much more besides) about the
project in future.

This email is confidential and intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient, be advised that you have received this email in error and that any use, disclosure, copying or distribution or any action taken or omitted to be taken in reliance on it is strictly prohibited. If you have received this email in error please contact the sender. Any views or opinions presented in this email are solely those of the author and do not necessarily represent those of Praxis. 

Although this email and any attachments are believed to be free of any virus or other defect, no responsibility is accepted by Praxis or any of its associated companies for any loss or damage arising in any way from the receipt or use thereof. The IT Department at Praxis can be contacted at it.support@xxxxxx

Praxis High Integrity Systems Ltd:

Company Number: 3302507, registered in England and Wales

Registered Address: 20 Manvers Street, Bath. BA1 1PX

VAT Registered in Great Britain: 682635707