Programmentwicklung und Verifikation: Springers Angewandte Informatik
Autor Gerald Futschekde Limba Germană Paperback – 23 mar 1989
Din seria Springers Angewandte Informatik
- 20% Preț: 352.95 lei
- 20% Preț: 351.48 lei
- 20% Preț: 354.08 lei
- 20% Preț: 351.16 lei
- 20% Preț: 349.70 lei
- 20% Preț: 352.62 lei
- 20% Preț: 498.83 lei
- 20% Preț: 352.95 lei
- 20% Preț: 349.70 lei
- 20% Preț: 350.52 lei
- 20% Preț: 350.52 lei
- 20% Preț: 351.48 lei
- 20% Preț: 360.38 lei
- 20% Preț: 349.24 lei
- 20% Preț: 352.30 lei
- 20% Preț: 357.97 lei
- 20% Preț: 357.01 lei
Preț: 434.18 lei
Preț vechi: 542.71 lei
-20% Nou
Puncte Express: 651
Preț estimativ în valută:
83.09€ • 86.31$ • 69.02£
83.09€ • 86.31$ • 69.02£
Carte tipărită la comandă
Livrare economică 03-17 februarie 25
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783211818671
ISBN-10: 3211818677
Pagini: 204
Ilustrații: IX, 183 S.
Dimensiuni: 170 x 244 x 11 mm
Greutate: 0.33 kg
Editura: SPRINGER VIENNA
Colecția Springer
Seria Springers Angewandte Informatik
Locul publicării:Vienna, Austria
ISBN-10: 3211818677
Pagini: 204
Ilustrații: IX, 183 S.
Dimensiuni: 170 x 244 x 11 mm
Greutate: 0.33 kg
Editura: SPRINGER VIENNA
Colecția Springer
Seria Springers Angewandte Informatik
Locul publicării:Vienna, Austria
Public țintă
ResearchCuprins
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 Für und wider Verifizieren.- 2. Einführende Beispiele.- 2.1 Mischen zweier sortierter Karteikartenstapel.- 2.2 Diskussion der Art der Präsentation des Verfahrens.- 2.3 Sortieren durch Mischen.- 2.4 Invarianten als Lösung von Rätselaufgaben.- 3. Zusicherungen (Assertions).- 3.1 Zusicherungen als Dokumentation von Programmen.- 3.2 Die Sprache der Zusicherungen.- 4. Programmzustände und Zustandsraum.- 4.1 Der Zusammenhang zwischen Zuständen und Zusicherungen.- 4.2 Programme als Abbildungen im Zustandsraum.- 5. Spezifizieren von Programmen.- 5.1 Spezifizieren mit Pre- und Postcondition.- 5.2 Beispiele für Spezifikationen.- 6. Verifikationsregeln (Verification rules).- 6.1 Konsequenz-Regeln.- 6.2 Die Zuweisung.- 6.3 Die Sequenz.- 6.4 Die Alternative (if-Anweisung).- 6.5 Die Iteration (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.- 8. Die schwächste Precondition (weakest precondition).- 8.1 Verifikation mit wp.- 8.2 Die wp der einzelnen Anweisungen.- 8.3 Die wp als Prädikatentransformation.- 8.4 Definition der Semantik mit Hilfe der schwächsten Precondition.- 8.5 Eigenschaften der wp.- 8.6 Die schwächste Precondition für die Termination.- 9. Beispiele für Programmentwicklungen.- 9.1 Sortieren von Feldern.- 9.2 Binäre 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 beiWertpapieren.- 10. Unterprogramme (Prozeduren).- 10.1 Die Prozedurdeklaration.- 10.2 Der Prozeduraufruf.- 10.3 Die schwächste 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 für inverse Anweisungen.- 11.2 Invertieren der zusammengesetzten Anweisung.- 11.3 Invertieren der alternativen Anweisung.- 11.4 Invertieren von Schleifen.- 11.5 Eine Analogie zum täglichen Leben.- 12. Parallele Programme.- 12.1 Zusammensetzen von parallelen Programmen.- 12.2 Beispiele für parallele Programme.- A. Lösungen der Aufgaben.- B. Syntax der Zusicherungen.- C. Verifikationsregeln und wp.- D. Aufwand von Verfahren.