Overview

Full Product Details

Author:   Gerald Futschek
Publisher:   Springer Verlag GmbH
Imprint:   Springer Verlag GmbH
Dimensions:   Width: 17.00cm , Height: 1.10cm , Length: 24.40cm
Weight:   0.410kg
ISBN:  

9783211818671

ISBN 10:   3211818677
Pages:   183
Publication Date:   23 March 1989
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   Out of stock  
The supplier is temporarily out of stock of this item. It will be ordered for you on backorder and shipped when it becomes available.
Language:   German

Table of Contents

1. Warum Verifizieren von Programmen?.- 1.1 Korrektheit von Programmen.- 1.2 Verifizieren versus Testen von Programmen.- 1.3 Programme gleichzeitig entwickeln und verifizieren.- 1.4 Fur und wider Verifizieren.- 2. Einfuhrende Beispiele.- 2.1 Mischen zweier sortierter Karteikartenstapel.- 2.2 Diskussion der Art der Prasentation des Verfahrens.- 2.3 Sortieren durch Mischen.- 2.4 Invarianten als Loesung von Ratselaufgaben.- 2.4.1 Weinpantschen.- 2.4.2 Hofstadters MU-Ratsel.- 3. Zusicherungen (Assertions).- 3.1 Zusicherungen als Dokumentation von Programmen.- 3.2 Die Sprache der Zusicherungen.- 3.2.1 Zusicherungen als Boolesche Ausdrucke.- 3.2.2 Die Zusicherungen true und false.- 3.2.3 Zusicherungen mit Quantoren.- 3.2.4 Selbstdefinierte Pradikate.- 3.2.5 Selbstdefinierte arithmetische Funktionen.- 4. Programmzustande und Zustandsraum.- 4.1 Der Zusammenhang zwischen Zustanden und Zusicherungen.- 4.2 Programme als Abbildungen im Zustandsraum.- 5. Spezifizieren von Programmen.- 5.1 Spezifizieren mit Pre- und Postcondition.- 5.2 Beispiele fur Spezifikationen.- 6. Verifikationsregeln (Verification rules).- 6.1 Konsequenz-Regeln.- 6.2 Die Zuweisung.- 6.2.1 Die Zuweisung an eine einfache Variable.- 6.2.2 Die Mehrfachzuweisung.- 6.3 Die Sequenz.- 6.4 Die Alternative (if-Anweisung).- 6.5 Die Iteration (Schleife).- 6.5.1 Die while-Schleife.- 6.5.2 Die repeat-Schleife.- 6.6 Termination von Schleifen.- 6.7 Verifikation der while-Schleife.- 7. Entwickeln von Schleifen.- 7.1 Entwickeln einer Schleife aus einer gegebenen Invariante und Terminationsfunktion.- 7.2 Entwickeln von Invarianten aus gegebenen Spezifikationen.- 7.2.1 Die Invariante als Verallgemeinerung der Postcondition.- 7.2.2 Weglassen einer Bedingung.- 7.2.3 Konstante durch Variable ersetzen und Bereich der Variablen angeben.- 7.2.4 Kombinieren von Pre- und Postcondition.- 8. Die schwachste Precondition (weakest precondition).- 8.1 Verifikation mit wp.- 8.2 Die wp der einzelnen Anweisungen.- 8.2.1 wp der Leeranweisung.- 8.2.2 wp der Zuweisung.- 8.2.3 wp der Mehrfachzuweisung.- 8.2.4 wp der Sequenz.- 8.2.5 wp der Alternative.- 8.2.6 wp der Iteration.- 8.3 Die wp als Pradikatentransformation.- 8.4 Definition der Semantik mit Hilfe der schwachsten Precondition.- 8.5 Eigenschaften der wp.- 8.6 Die schwachste Precondition fur die Termination.- 9. Beispiele fur Programmentwicklungen.- 9.1 Sortieren von Feldern.- 9.1.1 Sortieren durch direktes Einfugen.- 9.1.2 Sortieren durch Minimumsuche.- 9.2 Binare Suche in einem Feld.- 9.3 Die Datenstruktur Heap (Halde).- 9.4 Heapsort.- 9.5 Die M kleinsten Elemente von N Elementen.- 9.6 Maximaler Kursgewinn bei Wertpapieren.- 10. Unterprogramme (Prozeduren).- 10.1 Die Prozedurdeklaration.- 10.2 Der Prozeduraufruf.- 10.3 Die schwachste Precondition des Prozeduraufrufs.- 10.4 Verifikation des Prozeduraufrufs.- 10.5 Spezifikation des Prozedurrumpfes mit externen Variablen.- 10.6 Verwendung von Variablen-Parametern.- 10.7 Eine verallgemeinerte Konsequenz-Regel.- 11. Invertieren von Programmen.- 11.1 Beispiele fur inverse Anweisungen.- 11.2 Invertieren der zusammengesetzten Anweisung.- 11.3 Invertieren der alternativen Anweisung.- 11.4 Invertieren von Schleifen.- 11.5 Eine Analogie zum taglichen Leben.- 12. Parallele Programme.- 12.1 Zusammensetzen von parallelen Programmen.- 12.2 Beispiele fur parallele Programme.- 12.2.1 Summe der Elemente eines Feldes.- 12.2.2 Skalarprodukt zweier Vektoren.- 12.2.3 Matrixmultiplikation.- A. Loesungen der Aufgaben.- B. Syntax der Zusicherungen.- C. Verifikationsregeln und wp.- D. Aufwand von Verfahren.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions