The Object Z Specification Language

by Smith, Graeme

• ISBN13: 9780792386841
• ISBN10: 0792386841
• Format: Hardcover
• Copyright: 1999-10-01
• Publisher: Kluwer Academic Pub

Summary

Object-Z is an object-oriented extension of the formal specification language Z. It adds to Z notions of classes and objects, and inheritance and polymorphism. By extending Z's semantic basis, it enables the specification of systems as collections of independent objects in which self and mutual referencing are possible. The Object-Z Specification Language presents a comprehensive description of Object-Z including discussions of semantic issues, definitions of all language constructs, type rules and other rules of usage, specification guidelines, and a full concrete syntax. It will enable you to confidently construct Object-Z specifications and is intended as a reference manual to keep by your side as you use and learn to use Object-Z. The Object-Z Specification Language is suitable as a textbook or as a secondary text for a graduate-level course, and as a reference for researchers and practitioners in industry.

Table of Contents

Preface	xi
Introduction	1	(26)
Motivation	2	(2)
Classes	4	(3)
Objects	7	(3)
Inheritance	10	(3)
Polymorphism	13	(1)
Case Study: Tetris	14	(13)
Semantic Basis	27	(16)
Object Identity	28	(4)
Types and Values	28	(2)
Forward declaration	30	(2)
Self-reference	32	(1)
Objects	32	(4)
Objects vs. object identities	33	(1)
Forward declaration revisited	34	(2)
Modularity and Compositionality	36	(7)
Object coupling	36	(2)
Object aliasing	38	(1)
Object containment	39	(4)
Syntactic Constructs	43	(32)
Class Definitions	44	(2)
Visibility Lists	46	(1)
Inherited Classes	46	(4)
Cancellation and redefinition of features	49	(1)
Local Definition	50	(2)
Basic types	50	(1)
Axiomatic definitions	50	(1)
Abbreviation definitons	51	(1)
Free types	51	(1)
State Schemas	52	(1)
Initial State Schemas	53	(1)
Operations	53	(15)
Operations schemas	54	(2)
Operation promotions	56	(1)
Operation operators	57	(5)
Distributed operators	62	(3)
Recursion	65	(3)
Predicates	68	(2)
Boolean-valued expressions	68	(1)
Promoted initial state predicates	69	(1)
Expressions	70	(5)
Class names	71	(1)
Polymorphism	71	(1)
Class union	72	(1)
Object containment	73	(1)
Promoted attributes	73	(1)
Self	74	(1)
Language Definition	75	(40)
Meta-Functions	76	(2)
Global Paragraphs	78	(3)
Class Paragraphs	81	(9)
Operation Expressions	90	(17)
Predicates	107	(2)
Expressions	109	(6)
Concurrent Systems	115	(18)
Aggregation	116	(2)
Synchronization	118	(1)
Communication	119	(1)
Nondeterminism	120	(2)
Case Study: Hearts	122	(11)
Concrete Syntax	133	(10)
Specifications	134	(1)
Global Paragraphs	134	(1)
Class Paragraphs	135	(1)
Operation Expressions	136	(1)
Schema Expressions	137	(1)
Declarations	138	(1)
Predicates	138	(1)
Expressions	139	(4)
Bibliography	143	(2)
Index	145