Anweisungen(II)

Maschine, Assembler: (un-)bedingter Sprung
strukturiert: Schleifen

Designfragen für Schleifen:

wie wird Schleife gesteuert? (Bedingung, Zähler, Daten, Zustand)
an welcher Stelle in der Schleife findet Steuerung statt (Anfang, Ende, dazwischen, evtl. mehreres)

Zähler
```
for p in 1 .. 10 loop .. end loop;
```

Daten

map (\x -> x*x) [1,2,3] ==> [1,4,9]
Collection<String> c 
    = new LinkedList<String> ();
for (String s : c) { ... }

Bedingung

while ( x > 0 ) { if ( ... ) { x = ... } ... }

Zustand (Iterator, hasNext, next)

Idee: vor Beginn steht Anzahl der Durchläufe fest.

richtig realisiert ist das nur in Ada:

for p in 1 .. 10 loop ... end loop;

Zähler p wird implizit deklariert
Zähler ist im Schleifenkörper konstant

Vergleiche (beide Punkte) mit Java, C++, C

Satz: Jedes Programm aus

Zuweisungen
Verzweigungen
Zählschleifen

terminiert (hält) für jede Eingabe.

Äquivalenter Begriff (für Bäume anstatt Zahlen): strukturelle Induktion (fold, Visitor, primitive Rekursion)

Satz: es gibt berechenbare Funktionen, die nicht primitiv rekursiv sind.

Beispiel: Interpreter für primitiv rekursive Programme.

Idee: führe für jeden Konstruktor eines algebraischen Datentyps (Liste, Baum) eine Rechnung/Aktion aus.

foreach, Parallel.Foreach,...

So:

interface Iterator<T> {
  boolean hasNext(); T next ();  }
interface Iterable<T> { 
   Iterator<T> iterator(); }
for (T x : ...) { ... }

Oder so:

public interface IEnumerator<T> : IEnumerator {
  bool MoveNext(); T Current { get; } }
interface IEnumerable<out T> : IEnumerable {
   IEnumerator<T> GetEnumerator() }
foreach (T x in ...) { ... }

(sieben Unterschiede ...)

using System.Collections.Generic;
public class it {
    public static IEnumerable<int> Data () {
        yield return 3;
        yield return 1;
        yield return 4;
    }
    public static void Main () {
        foreach (int i in Data()) {
            System.Console.WriteLine (i);
}   }   }

das ist die allgemeinste Form, ergibt (partielle) rekursive Funktionen, die terminieren nicht notwendig für alle Argumente.

Steuerung

am Anfang: while (Bedingung) Anweisung
am Ende: do Anweisung while (Bedingung)

Weitere Änderung des Ablaufes:

vorzeitiger Abbruch (break)
vorzeitige Wiederholung (continue)
beides auch nicht lokal

operationale Semantik durch Sprünge:

while (B) A;
==>
start : if (!B) goto end; 
        A; 
        goto start;
end   : skip;

(das ist auch die Notation der autotool-Aufgabe)

Ü: do A while (B);

...der Schleife

while ( B1 ) { 
   A1;
   if ( B2 ) break;
   A2;
}

...des Schleifenkörpers

while ( B1 ) { 
   A1;
   if ( B2 ) continue;
   A2;
}

manche Sprachen gestatten Markierungen (Labels) an Schleifen, auf die man sich in break beziehen kann:

foo : for (int i = ...) {
  bar : for (int j = ...) {

    if (...) break foo;

  }
}

Wie könnte man das simulieren?

bedingte, unbedingte (mit bekanntem Ziel)
- Maschinensprachen, Assembler, Java-Bytecode
- Fortran, Basic: if Bedingung then Zeilennummer
- Fortran: dreifach-Verzweigung (arithmetic-if)
``computed goto'' (Zeilennr. des Sprungziels ausrechnen)

man kann jedes while-Programm in ein goto-Programm übersetzen
und jedes goto-Programm in ein while-Programm ...
...das normalerweise besser zu verstehen ist.
strukturierte Programmierung = jeder Programmbaustein hat genau einen Eingang und genau einen Ausgang
aber: vorzeitiges Verlassen von Schleifen
aber: Ausnahmen (Exceptions)

Satz: zu jedem goto-Programm gibt es ein äquivalentes while-Programm.

Beweis-Idee: 1 : A1, 2 : A2; .. 5: goto 7; .. ⇒

while (true) {
  switch (pc) {
    case 1 : A1 ; pc++ ; break; ...
    case 5 : pc = 7 ; break; ... 
  }
}

Das nützt aber softwaretechnisch wenig, das übersetzte Programm ist genauso schwer zu warten wie das Original.

zu jedem while-Programm kann man ein äquivalentes angeben, das nur Verzweigungen (if) und Unterprogramme benutzt.

Beweis-Idee: while (B) A; ⇒

void s () {
    if (B) { A; s (); }
}

Anwendung: C-Programme ohne Schlüsselwörter.

vereinfachtes Modell, damit Eigenschaften entscheidbar werden (sind die Programme P₁, P₂ äquivalent?)

Syntax: Programme

Aktionen,
Zustandsprädikate (in Tests)
Sequenz/Block, if, goto/while.

Beispiel:

while (B && !C) { P; if (C) Q; }

Semantik des Programms P ist Menge der Spuren von P .

Spur = eine Folge von Paaren von Zustand und Aktion,
ein Zustand ist eine Belegung der Prädikatsymbole,
jede Aktion zerstört alle Zustandsinformation.

Satz: Diese Spursprachen (von goto- und while-Programmen) sind regulär.

Beweis: Konstruktion über endlichen Automaten.

Zustandsmenge = Prädikatbelegungen × Anweisungs-Nummer
Transitionen? (Beispiele)

Damit ist Spur-Äquivalenz von Programmen entscheidbar.
Beziehung zu tatsächlicher Äquivalenz?

http://www.imn.htwk-leipzig.de/~waldmann/edu/ws13/pps/umfrage/

2015-08-17