Preludium.- An Overview.- The Languages.- Abstract State Machines for the Classroom.- The event-B Modelling Method: Concepts and Case Studies.- A Methodological Guide to the CafeOBJ Logic.- Casl - the Common Algebraic Specification Language.- Duration Calculus.- The Logic of the RAISE Specification Language.- The Specification Language TLA+.- The Typed Logic of Partial Functions and the Vienna Development Method.- Z Logic and Its Applications.- Postludium.- Reviews.