Algebra and abstract data types. Signatures, sigma-algebras, categories, specification, signature-morphism, specification-morphism. Specification methods for abstract data types, class specification. A specification methodology for abstract data types: analysis of specification, analysis of representation and implementation. Proof methods for program correctness. Correctness of concurrent programs. A methodology for deriving correct concurrent programs. Data types in concurrent environment, synchronisation interface. Specification methods for synchronisation interface. Analysis of specification, proof of consistence problems.