Geschäftskunden Kundenprogramme
Vor Ort
Merkzettel Warenkorb
Programming with Specifications

Programming with Specifications

An Introduction to ANNA, A Language for Specifying Ada Programs

Aus der Reihe

Fr. 103.00

inkl. gesetzl. MwSt.
Versandkostenfrei
Gebundenes Buch

Gebundenes Buch

Fr. 103.00 Taschenbuch

Taschenbuch

Fr. 72.90 eBook

eBook

Fr. 62.90

Programming with Specifications

Ebenfalls verfügbar als:

Gebundenes Buch

Gebundenes Buch

ab Fr. 103.00
Taschenbuch

Taschenbuch

ab Fr. 72.90
eBook

eBook

ab Fr. 62.90

Beschreibung

Details

Einband

Gebundene Ausgabe

Erscheinungsdatum

23.10.1990

Verlag

Springer New York

Seitenzahl

416

Maße (L/B/H)

24/16/2.3 cm

Beschreibung

Details

Einband

Gebundene Ausgabe

Erscheinungsdatum

23.10.1990

Verlag

Springer New York

Seitenzahl

416

Maße (L/B/H)

24/16/2.3 cm

Gewicht

750 g

Auflage

1990

Sprache

Englisch

ISBN

978-0-387-97254-1

Weitere Bände von Monographs in Computer Science

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Erste Bewertung verfassen

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen filtern
  • Programming with Specifications
  • 0 What Anna Is.- 0.1 From Informal Comments to Formal Annotations.- 0.2 Adding Annotations to Ada.- 0.3 Applying Anna.- 0.4 Environments for Programming with Specifications.- 0.5 Future Developments.- 0.6 Terminology and Notation.- 1 Simple Annotations.- 1.1 Annotations.- 1.2 The Meaning of Simple Annotations.- 1.3 Anna Expressions.- 1.4 Quantified Expressions.- 1.5 Modifiers.- 1.6 Assertions.- 1.7 Compound Statement Annotations.- 1.8 Object Annotations.- 1.9 Subprogram Annotations.- 1.9.1 Out values of procedure parameters.- 1.9.2 Conformance of subprogram annotations.- 1.10 Type Annotations.- 1.10.1 Anna membership test.- 1.11 Elaboration of Annotations.- 1.12 Proper Annotations.- 2 Using Simple Annotations.- 2.1 Three General Activities.- 2.2 Virtual Text.- 2.2.1 Formalizing concepts.- 2.2.2 Rules for virtual text.- 2.3 Assertions as Tests and Documentation.- 2.3.1 Choosing assertions.- 2.3.2 When to use assertions to express tests.- 2.4 Assertions and Timing.- 2.5 Assertions in Loops.- 2.5.1 Successor functions.- 2.5.2 Related assertions.- 2.5.3 Structuring testing and proof.- 2.5.4 Loop induction.- 2.6 Invariants: Compound Statement Annotations.- 2.7 Increasing the Scope of Annotations.- 2.8 Specification Using Subprogram Annotations.- 2.8.1 Specifying subprograms.- 2.8.2 Formalizing and organizing concepts.- 2.9 Runtime Checking of Simple Annotations.- 3 Exceptions.- 3.1 Annotating Raising and Handling of Exceptions.- 3.1.1 Consistency of raising and handling exceptions.- 3.2 Propagation Annotations.- 3.3 Annotating Exception Propagation.- 4 Package Specifications.- 4.1 Annotations and Package Structure.- 4.2 Simple Annotations in Package Declarations.- 4.3 Package States.- 4.4 Using Package States.- 4.4.1 Evaluating package functions in a state.- 4.4.2 Successor states.- 4.4.3 Equality on state types.- 4.5 Package Axioms.- 4.5.1 Axioms for equality.- 4.6 Restrictions on Package States.- 4.6.1 Restrictions on use of state attributes.- 4.6.2 State attributes of generic packages.- 5 The Process of Specifying Packages.- 5.1 Getting Started.- 5.2 Theory Packages.- 5.3 A PL/1 String Manipulation Package.- 5.4 A Simple Sets Package.- 5.5 Dependent Specification.- 5.6 Relative Specification.- 5.6.1 Extension.- 5.6.2 Association—Modeling types with other types.- 5.6.3 An example of relative specification by association — Small Library.- 5.7 The DIRECT_IO Package.- 5.8 Symbolic Execution of Specifications.- 5.8.1 A recipe for symbolic execution.- 5.8.2 An example of symbolic execution.- 5.9 Iterators and Generators.- 6 Annotation of Generic Units.- 6.1 Generic Annotations.- 6.2 Generic Parameter Constraints.- 6.2.1 Rationale for restricting generic parameter annotations.- 6.3 Annotated Generic Units as Reusable Software.- 6.3.1 Generalization.- 6.3.2 Specifying generic contexts.- 6.3.3 Generic theories.- 7 Annotation of Operations on Composite Types.- 7.1 Array States.- 7.2 Using Array States: QuickSort.- 7.3 Record States.- 7.3.1 Variant record states.- 7.4 Access Types and Collections.- 7.4.1 Collections.- 7.4.2 Collection states and operations.- 7.5 Using Collections.- 8 Annotation of the Hidden Parts of Packages.- 8.1 Modified Type Annotations.- 8.1.1 Stability constraints.- 8.1.2 Changing values of composite types.- 8.1.3 Semantics of modified type annotations.- 8.2 Representation of Package States.- 8.2.1 Restrictions on using package states.- 8.2.2 Hidden state property.- 8.3 Annotation of Hidden Package States.- 8.4 Annotation of Package Subprogram Bodies.- 8.5 Establishing Consistency.- 8.6 Redefinition of Equality.- 8.7 Packages as Types.- 9 Interpretation of Package Specifications *.- 9.1 Why Interpretations Are Useful.- 9.2 Constructing Interpretations.- 9.3 Interpreting Subprogram Annotations.- 9.4 Full Specifications of Subprogram Bodies.- 9.5 Interpreting Package Axioms.- 9.6 Interpreting Dependent Specifications.- 10 Processes for Consistent Implementation of Packages.- 10.1 Making the Normal Ada Process More Rigorous.- 10.2 A Process Based on Runtime Checking.- 10.3 A Rigorous Process Based on Consistency Proof.- 10.4 An Example: Implementing a Package Body.- A Syntax.- B Tools.- B.1 The Anna Runtime Checking System.- B.2 Package Specification Analyzer.- C A Short Bibliography.- C.1 Anna.- C.2 Ada.- C.3 Specification Languages.- C.4 Formal Methods.- C.5 Testing.