Automation in the process of software development can result in significant gains in productivity. This course teaches a method - and associated toolkit - that supports such automation. The B-Method and B-Toolkit support formal specification, design, and code generation, as well as validation and verification. See also www.b-core.com

Course dates

Objectives

At the End of the course, students will be able to construct large software designs using a layered approach, and carry out a complete development from abstract specifications to running C code. They will also be able to animate and validate specifications, generate software modules, and create design documentation.

Contents

Basic specification concepts:

abstract machine notation; software modules; states and operations; proof obligations; substitutions; abstract machine initialisation; abstract machine parameterisation.

Specification construction:

Parallel substitutions as specification of operations; incremental specification construction techniques.

Program concepts:

algorithm development; sequencing; loops.

Program development:

data refinement; design techniques; layers of software; implementation; libraries.

Program generation:

entity relationship descriptions; rapid prototyping; test-bench generation.

Software engineering concepts:

separation of concerns; abstraction; information hiding; modularisation; stepwise refinement.

Mathematics:

predicate notation; machine-assisted proving; set notation; relations; functions; sequences.

Requirements

A working knowledge of discrete mathematics is assumed: Software Engineering Mathematics would be a suitable preparation.