Tutorium 11

Gruppen 2 und 4
Samuel Teuber
propa@teuber.dev
https://teuber.dev/propa

Übungsblätter

Umfrage

Vorbemerkungen

• CompletableFuture: get?

• Akka:
  • tell: Fire and forget
  • ask: Returns future

[INFO] [02/02/2021 09:52:40.111] [Main-akka.actor.default-dispatcher-4] [akka://Main/user/app/greeter] Message [java.lang.String] from Actor[akka://Main/user/app#-1020796728] to Actor[akka://Main/user/app/greeter#881124593] was not delivered. [1] dead letters encountered. If this is not an expected behavior, then [Actor[akka://Main/user/app/greeter#881124593]] may have terminated unexpectedly, This logging can be turned off or adjusted with configuration settings 'akka.log-dead-letters' and 'akka.log-dead-letters-during-shutdown'.

Aufgabe 1

/**
 * ...gibt null zurück, falls leer
 */
public Product takeSomeProduct();
/*@...
  @ requires product != null;
  @...
  @*/
public void put(Product product) { /*...*/}
// ...
cart.put(counter.takeSomeProduct());

Aufrufer verlezt Vertrag

Aufgabe 1

private Set<Product> products = new HashSet<Product>();
/*@...
  @ ensures getProducts().size() == \old(getProducts().size()) + 1;
  @...
  @*/
public void put(Product product) {
    products.add(product);
}
// ...
cart.put(counter.takeSomeProduct());

Aufgerufene Methode verletzt Vertrag

Aufgabe 2

/*@
  @ requires employee != null;
  @ requires !getEmployees().contains(employee);
  @ requires !employee.isEmployed();
  @ ensures employee.isEmployed();
  @ ensures getEmployees().size() == \old(getEmployees().size())+1;
  @ ensures getEmployees().containsAll(\old(getEmployees()));
  @*/
public void hire(Employee employee);

public void hire(Employee employee) {
    assert employee != null;
    assert !employees.contains(employee);
    assert !employee.isEmployed();
    List<Employee> oldEmployees = new ArrayList<>(employees);
    // ....
    assert employee.isEmployed();
    assert employees.size() == oldEmployees.size()+1;
    assert employees.containsAll(oldEmployees);
    assert employees.contains(employee);
}

Assert: Pro Contra

Pro

• Garantierte Kompatibilität mit Methode
• Während Programmausführung überprüfbar (-ca)
• Keine zusätzlichen Tools, Teil der Sprache

Contra

• Nur in Implementierung spezifizierbar
• Keine Schnittstellen spezifizierung (z.B. Interfaces)
• Zunächst nur während Laufzeit überprüfbar
• Möglichkeit bei "spezifizierung" die selben Denkfehler zu machen wie bei Programmierung (keine Trennung)

Aufgabe 3: Liskov

public class Rectangle {/*...*/}
public class Square extends Rectangle {/*...*/}

Problem:
Stärkere Vorbediungungen, Schwächere Nachbediungungen $$ \text{Precondition}_{super} \Rightarrow \text{Precondition}_{sub}\\ \text{Postcondition}_{sub} \Rightarrow \text{Postcondition}_{super} $$

Lösung:

• Shape Interface für area, eigene getter und setter
• AbstractRectangle, eigene getter und setter

Aufgabe 4.1: TeaseLisa

public class TeaseLisa {
    public static void main(String[] args) throws InterruptedException {
        ActorSystem actorSystem = ActorSystem.create("TeaseLisa");
        ActorRef lisa = actorSystem.actorOf(Props.create(Kids.class));
        lisa.tell("idiot", ActorRef.noSender());
        lisa.tell("muppet", ActorRef.noSender());
        lisa.tell("idiot", ActorRef.noSender());
        lisa.tell("muppet", ActorRef.noSender());
        Thread.sleep(1000);
        actorSystem.terminate();
    }
}

public class Kid extends AbstractActor {
    private int counter = 0;
    @Override
    public Receive createReceive() {
        return receiveBuilder()
            .match(String.class, this::handleMessage).build();
    }
    private void handleMessage(String message) {
        if (message.equals("idiot") || message.equals("muppet")) {
            counter++;
            if (counter > 3) {
                System.out.println("Muuhm!");
            } else {
                System.out.println("Stop it");
            }
        }
    }
}

Fragen?

Unifikation (1)

Substitution

$$ \sigma = \{X_2⇨X_1\}\\ \sigma\left(\ f\left(X_1, Y\right)=X_2\ \right) = f(X_1, Y)=X_1 $$

$$ \theta = \{X_1 ⇨ Y, Y ⇨ Z\}\\ \theta\left(\ \sigma\left(\ f\left(X_1, Y\right)=X_2\ \right)\ \right) = f(Y, Z)=Y $$

Eine Substitution wird überall, einmal, gleichzeitig durchgeführt!

$$ \theta \circ \sigma = \{ X_1 ⇨ Y, X_2 ⇨ Y, Y ⇨ Z \} $$

Gleichungssysteme

$$ X_1 = X_2\\ X_2 = X_3\\ X_3 = X_4 $$

Welche Substitution $\sigma$, damit das Gleichungssystem gültig ist?

Unifikation (2)

Komplexere Gleichungssysteme

$$ f(X_1,X_2,X_3) = Z\\ f(A,B,C) = X\\ X=Z $$

• Mit $X=Z$ $$ f(A,B,C)=f(X_1,X_2,X_3) $$

• Kann nur garantiert werden, wenn: $$ A=X_1\\ B=X_2\\ C=X_3 $$

• Unifikator: $$ \{X_1⇨A, X_2⇨B, X_3⇨C\}\circ \{X⇨f\left(A,B,C\right), Z⇨f\left(X_1,X_2,X_3\right)\} $$

Unifikation (3)

Most general unifier (mgu)

• Vorher: $$ \sigma = \{X_1⇨A, X_2⇨B, X_3⇨C, X⇨f\left(A,B,C\right), Z⇨f\left(A,B,C\right)\} $$
• Auch möglich: $$ \gamma = \{X_1⇨A, X_2⇨\color{red}{A}, X_3⇨\color{red}{A, B⇨A, C⇨A}, X⇨f\left(A,\color{red}{A,A}\right), Z⇨f\left(A,\color{red}{A,A}\right)\} $$

ABER: $$ \gamma = \{B⇨A, C⇨A\} \circ \sigma $$

$\sigma$ ist allgemeiner als $\gamma$

Wir nennen $\sigma$ den most general unifier (mgu), wenn für alle Unifikatoren $\gamma$ gilt es gibt einen zugehörigen Unifikator $\theta$, sodass: $$ \gamma = \theta \circ \sigma $$

Wie finden wir den mgu?

Algorithmische Lösung: Robinson

function unify(C) {
    if (C.empty()) {
        return []
    } else {
        (T1 = T2) := C.pop()
        if (T1 == T2)                     
        { return unify(C) }

        else if (T1.isVar() && !T2.isFree(T1)) 
        { return compose( unify([T1->T2]C), [T1->T2]) }

        else if (T2.isVar() && !T1.isFree(T2)) 
        { return compose( unify([T2->T1]C), [T2->T1]) }

        else {
            f(X1,...,XN) := T1
            g(Y1,...,YN) := T2
            if (g != f) { fail(); }
            else { return unify( C+[X1=Y1,...,XN=YN]) }
        }
    }
}

Robinson Algorithmus?

$$ C = \{\\ X_1 = f(X_2, X_3),\\ X_3 = g(X_4, X_5),\\ X_3 = g(X_7, X_5),\\ X_4 = X_5\\ \} $$

Typinferenz ohne Let

Veränderte Strategie:

• Konstruiere "Skelett" des Herleitungsbaums
  • Gleiche Regeln
  • Frische Variablen für Voraussetzungen
• Sammle Gleichungen, die erfüllt sein müssen
• Bestimme mgu des Gleichungssystems

Typinferenz mit Let

1. Berechne zunächst mgu $\sigma_{let}$ für Constraints aus linken LET Teilbaum ($C_{let}$)
2. Berechne $\tau = ta(\sigma_{let}(\tau_1),\sigma_{let}(\Gamma))$
3. Berechne rechten LET Teilbaum mit $\sigma_{let}(\Gamma) \cup \{f:\tau\}$

2 Bemerkungen

• VAR Regel: Ihr könnt auch einfach immer die erweiterete VAR Regel nutzen
  Wichtig ist nur, dass ihr wisst wie man das erweiterte VAR für instanziierte Typen nutzt
• Unterscheide: Herleiten vs. Angeben