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 forgetask: 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?¶
$$
\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?
- 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)\} $$
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¶
- Berechne zunächst mgu $\sigma_{let}$ für Constraints aus linken LET Teilbaum ($C_{let}$)
- Berechne $\tau = ta(\sigma_{let}(\tau_1),\sigma_{let}(\Gamma))$
- 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