Atjaunināt sīkdatņu piekrišanu

E-grāmata: Programmentwicklung und Verifikation

  • Formāts: PDF+DRM
  • Sērija : Springers Angewandte Informatik
  • Izdošanas datums: 13-Mar-2013
  • Izdevniecība: Springer Verlag GmbH
  • Valoda: ger
  • ISBN-13: 9783709187951
Citas grāmatas par šo tēmu:
  • Formāts - PDF+DRM
  • Cena: 33,70 €*
  • * ši ir gala cena, t.i., netiek piemērotas nekādas papildus atlaides
  • Ielikt grozā
  • Pievienot vēlmju sarakstam
  • Šī e-grāmata paredzēta tikai personīgai lietošanai. E-grāmatas nav iespējams atgriezt un nauda par iegādātajām e-grāmatām netiek atmaksāta.
  • Formāts: PDF+DRM
  • Sērija : Springers Angewandte Informatik
  • Izdošanas datums: 13-Mar-2013
  • Izdevniecība: Springer Verlag GmbH
  • Valoda: ger
  • ISBN-13: 9783709187951
Citas grāmatas par šo tēmu:

DRM restrictions

  • Kopēšana (kopēt/ievietot):

    nav atļauts

  • Drukāšana:

    nav atļauts

  • Lietošana:

    Digitālo tiesību pārvaldība (Digital Rights Management (DRM))
    Izdevējs ir piegādājis šo grāmatu šifrētā veidā, kas nozīmē, ka jums ir jāinstalē bezmaksas programmatūra, lai to atbloķētu un lasītu. Lai lasītu šo e-grāmatu, jums ir jāizveido Adobe ID. Vairāk informācijas šeit. E-grāmatu var lasīt un lejupielādēt līdz 6 ierīcēm (vienam lietotājam ar vienu un to pašu Adobe ID).

    Nepieciešamā programmatūra
    Lai lasītu šo e-grāmatu mobilajā ierīcē (tālrunī vai planšetdatorā), jums būs jāinstalē šī bezmaksas lietotne: PocketBook Reader (iOS / Android)

    Lai lejupielādētu un lasītu šo e-grāmatu datorā vai Mac datorā, jums ir nepieciešamid Adobe Digital Editions (šī ir bezmaksas lietotne, kas īpaši izstrādāta e-grāmatām. Tā nav tas pats, kas Adobe Reader, kas, iespējams, jau ir jūsu datorā.)

    Jūs nevarat lasīt šo e-grāmatu, izmantojot Amazon Kindle.

Die entscheidenden Argumente für die Korrektheit eines Programms können am einfachsten schon bei seiner Entwicklung festgehalten werden. Die Methoden, mit denen man den Korrektheitsbeweis Hand in Hand mit der Programmentwicklung führt, werden in diesem Buch beschrieben. Die Programme und die Informationen für die Verifikation werden mit eigens zu diesem Zweck erweiterten Struktogrammen dargestellt. Die Methoden und die zahlreichen Beispiele sind unabhängig von einer bestimmten Programmiersprache. Das Buch wendet sich nicht nur an die an Programmverifikation interessierten Leser, sondern an alle, die ein tieferes Verständnis von Programmen erreichen wollen. Der Leser soll die vorgestellten Methoden und Denkweisen bei der Entwicklung seiner eigenen Programme anwenden lernen, um so effizientere und sicherere Software zu erzeugen.
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.