Verlässliche Echtzeitsysteme

Please download to get full document.

View again

of 82
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Categories
Published
Verlässliche Echtzeitsysteme Programmfehler und Verifikation funktionaler Eigenschaften Peter Ulbrich Friedrich-Alexander-Universität Erlangen-Nürnberg Lehrstuhl Informatik 4 (Verteilte Systeme und Betriebssysteme)
Verlässliche Echtzeitsysteme Programmfehler und Verifikation funktionaler Eigenschaften Peter Ulbrich Friedrich-Alexander-Universität Erlangen-Nürnberg Lehrstuhl Informatik 4 (Verteilte Systeme und Betriebssysteme) www4.informatik.uni-erlangen.de 12. Mai 2015 Übersicht der heutigen Vorlesung Erster Schritt: Abwesenheit von Laufzeitfehlern beweisen Abstrakte Interpretation des Programmcodes Abstrakte Semantik Weitgehend automatisierbar für nicht-funktionale Eigenschaften Salopp: Verlässlichkeit von C auf das Niveau einer typsicheren Sprache bringen Verifikation funktionaler Eigenschaften: Design-by-Contract Grundlage: Zusagen in Form von Vor- und Nachbedingungen Wie beschreibt man diese Verträge? Prädikatenlogik Wie leitet man daraus Korrektheitsaussagen ab? Hoare- / WP-Kalkül Beschreibung von Verträgen mit Hilfe von Annotationen Beispielsweise durch eine Erweiterung der Programmiersprache Überprüft mithilfe eines Verifikationswerkzeugs 1 Übersicht 2/36 Gliederung 1 Übersicht 2 Laufzeitfehler 3 Design-by-Contract Problemstellung Grundlagen Hoare-Kalkül WP-Kalkül 4 Zusammenfassung 2 Laufzeitfehler 3/36 Astreé: Laufzeitfehler in C Undefiniertes Verhalten ist das Problem Generell: Undefiniertes Verhalten in C hat Seiteneffekte! Undefiniert mit ungewissem Ausgang Fehlerhafte Zugriffe, Überschreitung von Array-Grenzen, hängende Zeiger,... Ausnahmen durch Division durch 0, Gleitkommaoperation-Fehler,... Abbruch der Analyse Undefiniert mit vorhersagbarem Ausgang Ganzzahlüberlauf Fehlerhafte Verschiebungen (, ), Typumwandlung,... Analyse muss auf mögliche Ausgänge hin ausgedehnt werden 2 Laufzeitfehler 4/36 Astreé: Laufzeitfehler in C Undefiniertes Verhalten ist das Problem Generell: Undefiniertes Verhalten in C hat Seiteneffekte! Undefiniert mit ungewissem Ausgang Fehlerhafte Zugriffe, Überschreitung von Array-Grenzen, hängende Zeiger,... Ausnahmen durch Division durch 0, Gleitkommaoperation-Fehler,... Abbruch der Analyse Undefiniert mit vorhersagbarem Ausgang Ganzzahlüberlauf Fehlerhafte Verschiebungen (, ), Typumwandlung,... Analyse muss auf mögliche Ausgänge hin ausgedehnt werden Externes Wissen kann der Analyse helfen Wertebereich einschränken Anwendungsspezifisches Wissen (Algorithmus behandelt Überlauf) Präzision der Analyse steuern 2 Laufzeitfehler 4/36 Beispiel: Schleifen ausrollen 1 int main () 2 { 3 unsigned int flag = 0; 4 float x =0.0, y =0.0; 5 6 for ( unsigned int i = 0, i 10, i ++) { 7 if ( flag ) { 8 x += x/ y; 9 } else { 10 flag = 1; x = 1.0; y = 2.0; 11 } 12 } 13 } Semantic Loop Unrolling Pfadpräfixe (s. V/20 ff) abstrahieren von den Schleifendurchläufen Der Schleifenrumpf wird im Extremfall auf einen Pfad reduziert i = [0, 9], flag = [0, 1], y = [0, 2.0] 2 Laufzeitfehler 5/36 Beispiel: Schleifen ausrollen 1 int main () 2 { 3 unsigned int flag = 0; 4 float x =0.0, y =0.0; 5 6 for ( unsigned int i = 0, i 10, i ++) { 7 if ( flag ) { 8 x += x/ y; 9 } else { 10 flag = 1; x = 1.0; y = 2.0; 11 } 12 } 13 } Semantic Loop Unrolling Pfadpräfixe (s. V/20 ff) abstrahieren von den Schleifendurchläufen Der Schleifenrumpf wird im Extremfall auf einen Pfad reduziert i = [0, 9], flag = [0, 1], y = [0, 2.0] Ausrollen liefert zusätzliche Informationen Unterscheidung in ersten und zweiten Durchlauf verhindert den Fehlalarm 1) i = 0, flag = 0 2) i = [1, 9], flag = 1, y = 2.0 Erhöht jedoch die Kosten dramatisch (vgl. Pfadabdeckung IV/16) 2 Laufzeitfehler 5/36 Beispiel: Partitionierung 1 unsigned int foo ( int cond ) { 2 if ( cond ) { 3 x = 10; 4 y = 5; 5 } else { 6 x = 20; 7 y = 16; 8 9 } return x - y; 10 } Sammelsemantik (s. V/15 ff) fasst Pfade zusammen Hier kann der Unterlauf nicht ausgeschlossen werden Rückgabewert = [ 6, 15] 2 Laufzeitfehler 6/36 Beispiel: Partitionierung 1 unsigned int foo ( int cond ) { 2 if ( cond ) { 3 x = 10; 4 y = 5; 5 } else { 6 x = 20; 7 y = 16; 8 9 } return x - y; 10 } Sammelsemantik (s. V/15 ff) fasst Pfade zusammen Hier kann der Unterlauf nicht ausgeschlossen werden Rückgabewert = [ 6, 15] Selektive Partitionierung des Kontrollflusses Weist die Analyse an, Pfade getrennt zu verfolgen cond: Rückgabewert = 5,!cond: Rückgabewert = 4 Wiederrum auf Kosten der Komplexität 2 Laufzeitfehler 6/36 Gliederung 1 Übersicht 2 Laufzeitfehler 3 Design-by-Contract Problemstellung Grundlagen Hoare-Kalkül WP-Kalkül 4 Zusammenfassung 3 Design-by-Contract 7/36 Wiederholung: Fehlersuche in C-Programmen Diese Programm enthält diverse Fehler... Division durch 0, undefinierte Speicherzugriffe, Ganzzahlüberlauf 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) 3 { 4 unsigned int temp = 0; 5 6 for ( unsigned int i = 0; i size ; i ++) { 7 temp += array [ i]; 8 } 9 10 return temp / size ; 11 } Abstrakte Interpretation deckt diese Defekte auf Intervallanalyse erfasst z.b.... Den Wert 0 für size... Oder den möglichen Überlauf von temp 3 Design-by-Contract 3.1 Problemstellung 8/36 Ein korrekt(er)es C-Programm Vermeidung von Laufzeitfehlern ist nur die halbe Miete Wir können diese Fehler beheben! Zumindest für Spezialfälle ist dies offensichtlich 1 unsigned int average ( unsigned int [16] array ) { 2 unsigned long long temp = 0; 3 4 for ( unsigned int i = 0; i 16; i ++) { 5 temp += array [ i]; 6 } 7 8 return temp /20; 9 } 3 Design-by-Contract 3.1 Problemstellung 9/36 Ein korrekt(er)es C-Programm Vermeidung von Laufzeitfehlern ist nur die halbe Miete Wir können diese Fehler beheben! Zumindest für Spezialfälle ist dies offensichtlich 1 unsigned int average ( unsigned int [16] array ) { 2 unsigned long long temp = 0; 3 4 for ( unsigned int i = 0; i 16; i ++) { 5 temp += array [ i]; 6 } 7 8 return temp /20; 9 } Aber: Ist diese Implementierung korrekt? Mit Sicherheit nicht sie liefert einen vollkommen falschen Wert Wir müssen beschreiben, was wir von average erwarten! 3 Design-by-Contract 3.1 Problemstellung 9/36 Was der Entwickler wirklich will! Frei nach der libjustdoit-manier 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) { 3 unsigned long long temp = 0; 4 for ( unsigned int i = 0; i size ; i ++) { 5 temp += array [ i]; 6 } 7 return temp / size ; 8 } average liefert den Durchschnittswert aller Elemente des Felds array 3 Design-by-Contract 3.2 Grundlagen 10/36 Was der Entwickler wirklich will! Frei nach der libjustdoit-manier 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) { 3 unsigned long long temp = 0; 4 for ( unsigned int i = 0; i size ; i ++) { 5 temp += array [ i]; 6 } 7 return temp / size ; 8 } average liefert den Durchschnittswert aller Elemente des Felds array das ist die Nachbedingung Sie wird durch die Implementierung der Funktion garantiert der Aufrufer von average kann diese Nachbedingung ausnutzen 3 Design-by-Contract 3.2 Grundlagen 10/36 Was der Entwickler wirklich will! Frei nach der libjustdoit-manier die Funktion average stellt Forderungen an den Aufrufer Das Feld array hat genau size korrekt initialisierte Elemente Insbesondere sind keine leeren Felder erlaubt (size 0) temp darf nicht überlaufen sum(array,size) = ULONG_MAX 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) { 3 unsigned long long temp = 0; 4 for ( unsigned int i = 0; i size ; i ++) { 5 temp += array [ i]; 6 } 7 return temp / size ; 8 } average liefert den Durchschnittswert aller Elemente des Felds array das ist die Nachbedingung Sie wird durch die Implementierung der Funktion garantiert der Aufrufer von average kann diese Nachbedingung ausnutzen 3 Design-by-Contract 3.2 Grundlagen 10/36 Was der Entwickler wirklich will! Frei nach der libjustdoit-manier die Funktion average stellt Forderungen an den Aufrufer Das Feld array hat genau size korrekt initialisierte Elemente Insbesondere sind keine leeren Felder erlaubt (size 0) temp darf nicht überlaufen sum(array,size) = ULONG_MAX das sind die Vorbedingungen Der Aufrufer von average muss sie sicherstellen die Implementierung der Funktion kann sie ausnutzen 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) { 3 unsigned long long temp = 0; 4 for ( unsigned int i = 0; i size ; i ++) { 5 temp += array [ i]; 6 } 7 return temp / size ; 8 } average liefert den Durchschnittswert aller Elemente des Felds array das ist die Nachbedingung Sie wird durch die Implementierung der Funktion garantiert der Aufrufer von average kann diese Nachbedingung ausnutzen 3 Design-by-Contract 3.2 Grundlagen 10/36 Man ist vertraglich gebunden... Zusicherungen (engl. assertions) Regeln das Verhältnis zwischen Aufrufer und Prozedur 3 Design-by-Contract 3.2 Grundlagen 11/36 Man ist vertraglich gebunden... Zusicherungen (engl. assertions) Regeln das Verhältnis zwischen Aufrufer und Prozedur Vorbedingungen (engl. preconditions) P Werden vom Aufrufer erfüllt, in der Prozedur genutzt Nachbedingungen (engl. postconditions) Q Werden von der Prozedur erfüllt, vom Aufrufer genutzt Unter der Bedingung, dass die Vorbedingungen beim Prozeduraufruf gelten Invarianten (engl. invariants) I Gelten sowohl vor als auch nach dem Prozeduraufruf Eine zwischenzeitliche Verletzung innerhalb der Prozedur wird toleriert 3 Design-by-Contract 3.2 Grundlagen 11/36 Man ist vertraglich gebunden... Zusicherungen (engl. assertions) Regeln das Verhältnis zwischen Aufrufer und Prozedur Vorbedingungen (engl. preconditions) P Werden vom Aufrufer erfüllt, in der Prozedur genutzt Nachbedingungen (engl. postconditions) Q Werden von der Prozedur erfüllt, vom Aufrufer genutzt Unter der Bedingung, dass die Vorbedingungen beim Prozeduraufruf gelten Invarianten (engl. invariants) I Gelten sowohl vor als auch nach dem Prozeduraufruf Eine zwischenzeitliche Verletzung innerhalb der Prozedur wird toleriert Salopp formuliert, heißt das: Prozeduraufrufe sind Anweisungen (engl. statements) Bezeichnung S P I S Q I Nimmt man Vorbedingungen, Invarianten und die Prozedur zusammen, kommt man bei den Nachbedingungen und den Invarianten heraus 3 Design-by-Contract 3.2 Grundlagen 11/36 Zusicherungen... geht das einfach mit asserts? Vorbedingungen lassen sich durch assert-anweisungen prüfen: 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) { 3 unsigned long long temp = 0; 4 assert ( size 0); 5 6 for ( unsigned int i = 0; i size ; i ++) { 7 8 temp += array [ i]; 9 } unsigned int result = temp / size ; return result ; 15 } 3 Design-by-Contract 3.2 Grundlagen 12/36 Zusicherungen... geht das einfach mit asserts? Vorbedingungen lassen sich durch assert-anweisungen prüfen: 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) { 3 unsigned long long temp = 0; 4 assert ( size 0); 5 6 for ( unsigned int i = 0; i size ; i ++) { 7 assert ( temp = ULONG_MAX - array [ i ]); 8 temp += array [ i]; 9 } unsigned int result = temp / size ; return result ; 15 } auch (Schleifen)invarianten lassen sich so handhaben 3 Design-by-Contract 3.2 Grundlagen 12/36 Zusicherungen... geht das einfach mit asserts? Vorbedingungen lassen sich durch assert-anweisungen prüfen: 1 unsigned int average ( unsigned int * array, 2 unsigned int size ) { 3 unsigned long long temp = 0; 4 assert ( size 0); 5 6 for ( unsigned int i = 0; i size ; i ++) { 7 assert ( temp = ULONG_MAX - array [ i ]); 8 temp += array [ i]; 9 } unsigned int result = temp / size ; 12 assert ( result == average_2 ( array, size )); return result ; 15 } auch (Schleifen)invarianten lassen sich so handhaben problematisch sind vor allem Nachbedingungen Nachbedingungen werden deklarativ beschrieben In assert-anweisung wird der Wert typischerweise explizit konstruiert Begrenzungen sind identisch zu klassischen Tests Sinnvoll, um das Vorhandensein von Defekten zu demonstrieren,... 3 Design-by-Contract 3.2 Grundlagen 12/36 Sir Charles Anthony Richard (C.A.R.) Hoare Ein Informatik-Pionier: Leben und Wirken 1934 geboren in Colombo, Sri Lanka ab 1956 Studium in Oxford und Moskau ab 1960 Elliot Brothers 1968 Habilitation an der Queen s University of Belfast ab 1977 Professor für Informatik (Oxford) Auszeichnungen (Auszug) 1980 Turing Award 2000 Kyoto-Preis 2007 Friedrich L. Bauer Preis 2010 John-von-Neumann-Medaille bekannte Werke (Auszug) Quicksort-Algorithmus [5] Hoare-Kalkül [6] Communicating Sequential Processes [7] 3 Design-by-Contract 3.3 Hoare-Kalkül 13/36 Wie gibt man Zusicherungen an? Zusicherungen werden als Formeln der Prädikatenlogik beschrieben üblicherweise gibt man sie als sog. Hoare-Triple an: {P} S {Q} P ist die Vorbedingung,Q die Nachbedingung, S ein Programmsegment P und Q werden als Formeln der Prädikatenlogik beschrieben Bedeutung: Falls P vor der Ausführung von S gilt, gilt Q danach Dies setzt vorraus, dass S terminiert sonst ist keine Aussage über den folgenden Programmzustand möglich partielle Korrektheit: die Terminierung muss gesondert bewiesen werden Man verwendet {P} S {falsch} um auszudrücken, dass S nicht terminiert 3 Design-by-Contract 3.3 Hoare-Kalkül 14/36 Wie gibt man Zusicherungen an? (Forts.) Am Beispiel der Funktion int maximum(int a,int b) S :int maximum ( int a, int b) { int result = INT_MIN ; } if( a b) result = a; else result = b; return result ; Das Programmsegment ist die Implementierung der Funktion 3 Design-by-Contract 3.3 Hoare-Kalkül 15/36 Wie gibt man Zusicherungen an? (Forts.) Am Beispiel der Funktion int maximum(int a,int b) P : wahr S :int maximum ( int a, int b) { int result = INT_MIN ; } if( a b) result = a; else result = b; return result ; Das Programmsegment ist die Implementierung der Funktion Vorbedingung P : wahr die Implementierung stellt keine Anforderungen an die Parameter 3 Design-by-Contract 3.3 Hoare-Kalkül 15/36 Wie gibt man Zusicherungen an? (Forts.) Am Beispiel der Funktion int maximum(int a,int b) P : wahr S :int maximum ( int a, int b) { int result = INT_MIN ; if( a b) result = a; else result = b; return result ; } Q : result a result b Das Programmsegment ist die Implementierung der Funktion Vorbedingung P : wahr die Implementierung stellt keine Anforderungen an die Parameter Nachbedingung Q : result a result b offensichtliche Eigenschaft des zu berechnenden Ergebnisses 3 Design-by-Contract 3.3 Hoare-Kalkül 15/36 Wie gibt man Zusicherungen an? (Forts.) Am Beispiel der Funktion int maximum(int a,int b) P : wahr S :int maximum ( int a, int b) { int result = INT_MIN ; if( a b) result = a; else result = b; return result ; } Q : result a result b Das Programmsegment ist die Implementierung der Funktion Vorbedingung P : wahr die Implementierung stellt keine Anforderungen an die Parameter Nachbedingung Q : result a result b offensichtliche Eigenschaft des zu berechnenden Ergebnisses wie man dieses Ergebnis bestimmt, ist hier nicht von Belang 3 Design-by-Contract 3.3 Hoare-Kalkül 15/36 Wie überprüft man die Einhaltung der Zusicherungen? Aufgabe: Man muss P, S und Q zusammenbringen! 3 Design-by-Contract 3.3 Hoare-Kalkül 16/36 Wie überprüft man die Einhaltung der Zusicherungen? Aufgabe: Man muss P, S und Q zusammenbringen! Prädikattransformation (engl. predicate transformer semantics) Das Programmsegment S implementiert eine Transformation zwischen der Vorbedingung P und der Nachbedingung Q Entsprechende Transformationen existieren für alle Programmkonstrukte Zuweisungen, Sequenzen, Verzweigungen, Schleifen, Funktionsaufrufe,... 3 Design-by-Contract 3.3 Hoare-Kalkül 16/36 Wie überprüft man die Einhaltung der Zusicherungen? Aufgabe: Man muss P, S und Q zusammenbringen! Prädikattransformation (engl. predicate transformer semantics) Das Programmsegment S implementiert eine Transformation zwischen der Vorbedingung P und der Nachbedingung Q Entsprechende Transformationen existieren für alle Programmkonstrukte Zuweisungen, Sequenzen, Verzweigungen, Schleifen, Funktionsaufrufe,... stellen Strategien bereit, um Hoare-Triple {P} S {Q} zu beweisen Eine Vorwärtsanalyse liefert die stärkste Nachbedingung sp(s, P) (engl. Strongest postcondition, sp) {P} S {Q} gilt, genau dann wenn sp(s, P) Q wahr ist Eine Rückwärtsanalyse liefert die schwächste Vorbedingung wp(s, Q) (engl. Weakest precondition, wp) {P} S {Q} gilt, genau dann wenn P wp(s, Q) wahr ist 3 Design-by-Contract 3.3 Hoare-Kalkül 16/36 Wie überprüft man die Einhaltung der Zusicherungen? Aufgabe: Man muss P, S und Q zusammenbringen! Prädikattransformation (engl. predicate transformer semantics) Das Programmsegment S implementiert eine Transformation zwischen der Vorbedingung P und der Nachbedingung Q Entsprechende Transformationen existieren für alle Programmkonstrukte Zuweisungen, Sequenzen, Verzweigungen, Schleifen, Funktionsaufrufe,... stellen Strategien bereit, um Hoare-Triple {P} S {Q} zu beweisen Eine Vorwärtsanalyse liefert die stärkste Nachbedingung sp(s, P) (engl. Strongest postcondition, sp) {P} S {Q} gilt, genau dann wenn sp(s, P) Q wahr ist Eine Rückwärtsanalyse liefert die schwächste Vorbedingung wp(s, Q) (engl. Weakest precondition, wp) {P} S {Q} gilt, genau dann wenn P wp(s, Q) wahr ist Prädikattransformation basiert auf dem Hoare-Kalkül Beschreibt die (formale) Funktionssemantik eines Programms 3 Design-by-Contract 3.3 Hoare-Kalkül 16/36 Das Hoare-Kalkül Ein formales System, um Aussagen zur Korrektheit von Programmen zu treffen, die in imperativen Programmiersprachen verfasst sind. Das Hoare-Kalkül umfasst Axiome... Leere Anweisungen Zuweisungen... und Ableitungsregeln (bzw. Inferenzregeln) Sequenzen (bzw. Komposition) von Anweisungen Auswahlen von Anweisungen Iterationen von Anweisungen und Konsequenz Ist nicht vollständig und bezieht sich nur auf die partielle Korrektheit Andernfalls würde diese eine Lösung des Halteproblems bedeuten Terminierung ist daher gesondert nachzuweisen 3 Design-by-Contract 3.3 Hoare-Kalkül 17/36 Axiome Leere Anweisung skip {P}skip{P} Die leere Anweisung verändert den Programmzustand nicht falls P vor skip gilt, gilt es auch danach 3 Design-by-Contract 3.3 Hoare-Kalkül 18/36 Axiome Leere Anweisung skip {P}skip{P} Die leere Anweisung verändert den Programmzustand nicht falls P vor skip gilt, gilt es auch danach Zuweisung x = y {P [y/x]}x = y{p} P [y/x] jedes Auftreten von x in P wird durch y ersetzt was nach der Zuweisung für x gilt, galt vor der Zuweisung für y Beispiel: {y 100}x = y;{x 100} P : y 100 S : x = y; Q : x Design-by-Contract 3.3 Hoare-Kalkül 18/36 Sequenzregel Für lineare Kompositionen S 1 ; S 2 zweier Segmente S 1 und S 2 {P}S 1 {Q} {Q}S 2 {R} {P}S 1 ; S 2 {R} Falls S 1 die Vorbedingung für S 2 erzeugt, können sie verkettet werden Im Anschluss an S 2 hat dessen Nachbedingung R Bestand 3 Design-by-Contract 3.3 Hoare-Kalkül 19/36 Sequenzregel Für lineare Kompositionen S 1 ; S 2 zweier Segmente S 1 und S 2 {P}S 1 {Q} {Q}S 2 {R} {P}S 1 ; S 2 {R} Falls S 1 die Vorbedingung für S 2 erzeugt, können sie verkettet werden Im Anschluss an S 2 hat dessen Nachbedingung R Bestand Beispiel: {y + 1 = 43}x = y + 1;{x = 43} {x = 43}z = x;{z = 43} {y + 1 = 43}x = y + 1; z = x;{z = 43} 3 Design-by-Contract 3.3 Hoare-Kalkül 19/36 Sequenzregel Für lineare Kompositionen S 1 ; S 2 zweier Segmente S 1 und S 2 {P}S 1 {Q} {Q}S 2 {R} {P}S 1 ; S 2 {R} Falls S 1 die Vorbedingung für S 2 erzeugt, können sie verkettet werden Im Anschluss an S 2 hat dessen Nachbedingung R Bestand Beispiel: {y + 1 = 43}x = y + 1;{x = 43} {x = 43}z = x;{z = 43} {y + 1 = 43}x = y + 1; z = x;{z = 43} P : y + 1 = 43 S 1 :x = y + 1; Q : x = 43 Q : x = 43 S 2 :z = x; R : z = 43 P : y + 1 = 43 S 1 :x = y + S 2 :z = x; 1; Q : z = 43 3 Design-by-Contract 3.3 Hoare-Kalkül 19/36 Auswahlregel Wie behandelt man Verzweigungen in if-else-anweisungen? Zwei alternative Programmsegmente S 1 und S 2 S :if(a b) result = a; else result = b; P : wahr Q :??? Auswahlregel Wie behandelt man Verzweigungen in if-else-anweisungen? Zwei alternative Programmsegmente S 1 und S 2 Diese werden durch eine Bedingung B unterschieden S 0 : if(a b) P : wahr S :if(a b) result = a; else result = b; Q :??? S 1 : result = a; else S 2 : result = b; Auswahlregel Wie behandelt man Verzweigungen in if-else-anweisungen? Zwei alternative Programmsegmente S 1 und S 2 Diese werden durch eine Bedingung B unterschieden Eingangs
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks