Anweisungen(II)

Designfragen für Schleifen:

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


richtig realisiert ist das nur in Ada:

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

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

Satz: Jedes Programm aus

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

Weitere Änderung des Ablaufes:

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);

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?

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 P1, P2 äquivalent?)

Syntax: Programme

Beispiel:

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

Semantik des Programms P ist Menge der Spuren von P .

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

Beweis: Konstruktion über endlichen Automaten.

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