# Lösungsvorschlag Software Architecture And Engineering FS14

Achtung, dies ist nur ein von Studenten erstellter Lösungsvorschlag, keine offizielle Lösung.

### A. Modeling using UML and Alloy

1. R1, R2 & R3

#### (b)

sig ID{}
sig Client{}
sig Account{
id: one ID,
owner: one Client
}
sig Checking, Savings, CreditCard extends Account{}

fact atMostFiveAccounts {
//gibt sicher bessere Lösungen
all c:Client | all disj a1,a2,a3,a4,a5,a6 :Account | a1.owner = c && a2.owner = c && a3.owner = c && a4.owner = c && a5.owner = c implies a6.owner != c
// bessere Lösung:
all c:Client | #{a:Account | a.owner = c} <= 5
// noch kürzer:
all c: Client| # owner.c <= 5
// oder äquivalent:
all c: Client| #c.~owner <= 5
}

fact uniqueIDs {
all disj a1,a2: Account | a1.id != a2.id
// kürzer:
all i: ID | one id.i
}

fact noCreditCardIfNoChecking {
all cc: CreditCard | some c:Checking | cc.owner = c.owner
// different approach (not better, just different, may be useful to illustrate some operators)
all c: Client | no Checking <: (owner.c) => no CreditCard <: (owner.c)
// yet another approach
all a1: CreditCard | some a2: Checking | a2.owner = a1.owner
}


#### (c)

sig Account {
balance: Int
}

pred init[s: Account] {
s.balance = 0
}

pred deposit[s, s': Account, amount: Int] {
(amount >= 0) =>
s'.balance = plus[s.balance, amount]
else
s'.balance = s.balance
}

pred withdraw[s, s': Account, amount: Int] {
(amount >= 0 && s.balance >= amount) =>
s'.balance = minus[s.balance, amount]
else
s'.balance = s.balance
}

pred inv[s: Account] {
s.balance >= 0
}

assert neverNegative {
// (1)
all s:Account | init[s] => inv[s]
// (2)
all s1, s2:Account, a:int | (inv[s1] and deposit[s1,s2,a]) => inv[s2]
all s1, s2:Account, a:int | (inv[s1] and withdraw[s1,s2,a]) => inv[s2]
}
// alternatively:
assert neverNegative {
all s: Account | init[s] => inv[s]
all s, s': Account, a: int | inv[s] => (deposit[s, s', a] or withdraw[s,s',a]) => inv[s']
}


### B. Alloy Semantics

#### (a)

${\displaystyle I_{1},I_{2},I_{4}}$

#### (b)

(1): Es hält, da next für beide Nodes weder die leere Menge sein darf, noch sich selbst beinhalten, kann sie zwingendermassen nur die Menge mit nur der anderen Node drin sein. Somit kommt man mit 2 mal next immer wieder zurück auf sich selbst.

(2): Hier hält sie nicht mehr:
Node = {n0,n1,n2}
next = {(n0,n1),(n1,n0),(n2,n0)}
n2.next.next = n0.next = n1 != n2

### A. control flow graph

                                    +---------+
| b#start |
+---------+
|
|
↓
+-----+----------------------------+
| b#0 | int d = days; int y = 1980 |
+-----+----------------------------+
|
|
↓
+-----+--------------+           false
+ ---------------------------→| c#0 | c0 = 365 < d |----------------------------------------+
|                             +-----+--------------+                                        |
|                               |            ↑   ↑                                          |
|                          true |            |   |                                          |
|                               ↓            |   +----------+                               ↓
|         +-----+--------------------+       |              |        +-----+-----------------------------------------------+
|         | c#1 | c1 = isLeapYear(y) |       |              |        | b#4 | System.out.printf("year: %d, day: %d", y, d); |
|         +-----+--------------------+       |              |        +-----+-----------------------------------------------+
|             |                     |        | false        |                               |
|       false |                     | true   |              |                               |
|             ↓                     ↓        |              |                               ↓
+-----+-------------------------+  +-----+--------------+     |                           +-------+
| b#2 | d = d - 365; y = y + 1; |  | c#2 | c2 = 366 < d |     |                           | b#end |
+-----+-------------------------+  +-----+--------------+     |                           +-------+
|               |
| true          |
↓               |
+-----+-------------------------+
| b#3 | d = d - 366; y = y + 1; |
+-----+-------------------------+


### B. Coverage

(a) Block coverage: 1 = 100%

(b) Branch coverage: 5/6, da der false-Branch von c#2 nie genommen wird.

### C. smallest additional test input

Wie in B. berechnet, reicht der Test-Input 732 nicht um 100% Branch coverage zu erreichen. Wenn wir noch 366 dazu nehmen, reicht dies aber bereits, da 366 > 365 ist c#0 wahr, da 1980 % 4 = 0 und 1980 % 100 != 0, ist c#1 ebenfalls wahr, und da 366 nicht < 366 ist c#2 falsch und somit haben wir den letzten Branch auch noch genommen.

### D. Single Test with 100% Coverage

Nein, es gibt keinen einzelnen Input, der 100% Block Coverage & Branch Coverige erreichen kann. Denn um 100% Branch Coverage zu erreichen, müssen wir auch den false-Branch von c#2 nehmen. Um diesen zu nehmen brauchen wir irgendwann im Programmverlauf d = 366 und y = Schaltjahr. Wenn wir diesen Status aber haben, sind wir in einer Endlosschleife gefangen, da d immer grösser 365 ist, also c#0 immer wahr, y immer ein Schaltjahr ist, also c#1 ebenfalls immer wahr und d nie grösser als 366 ist ist c#2 immer falsch. Wenn wir also 100% Branch Coverage anstreben, können wir b#4 nie erreichen und 100% Block Coverage ist ausgeschlossen.

### E. Block Coverage -> Branch Coverage

Nein, wie in Task B zu sehen.

static void convert(int days) {
int d = days; int y = 1980;
while (365 < d) {
if (isLeapYear(y)) {
if (366 < d) {
d = d -366; y = y + 1;
}
// Beginn neuer Teil
else {
skip;
}
// Ende neuer Teil
} else {
d = d -365; y = y + 1;
}
}
System.out.printf("year: %d, day: %d", y, d);
}


### F. terminating

convert terminiert für alle Inputs bis auf ${\displaystyle k*366+(k-1)*3*365\forall k>0}$. von 1 bis 10'000 sind dies: 366, 1827, 3288, 4749, 6210, 7671 und 9132. Also 7 von 10'000 Zahlen, somit liegt die Wahrscheinlichkeit, dass convert nicht terminiert bei ${\displaystyle 7/10000=0.07\%}$

## Task 3 - Static analysis

### A. complete lattice

P und Q sind complete lattices.

### B. monotone

f ist nicht monoton, da ${\displaystyle P_{1,0}\sqsubseteq P_{2,0}{\text{ , aber }}f(P_{1,0})\sqsubseteq f(P_{2,0})}$ nicht gilt.

g ist monoton.

### C. abstract domain

when ${\displaystyle \alpha (f(\gamma (z)))\sqsubseteq g(z){\text{ for all }}z\in A}$

## Task 4 - Interval analysis

### A.

 Diese Aufgabe wurde noch von niemandem gelöst und wartet noch immer auf einen Musterlöser. Hast du dieses Fach bereits besucht? Hilf mit, die Qualität dieser Seite zu verbessern, indem du eine plausible Lösung für diese Frage notierst!

### B.

1. ${\displaystyle i\in [0,0],j\in [0,0],k\in [0,0]}$
2. ${\displaystyle i\in [0,0],j\in [0,0],k\in [0,0]}$
3. ${\displaystyle i\in [0,0],j\in [1,1],k\in [0,0]}$
4. ${\displaystyle i\in [0,33],j\in [-1,1],k\in [0,2]}$
5. ${\displaystyle i\in [0,31],j\in [-1,1],k\in [0,2]}$
6. ${\displaystyle i\in [0,31],j\in [-1,1],k\in [0,2]}$
7. ${\displaystyle i\in [0,31],j\in [-1,1],k\in [0,2]}$
8. ${\displaystyle i\in [0,33],j\in [-1,1],k\in [0,2]}$
9. ${\displaystyle i\in [0,33],j\in [-1,1],k\in [0,2]}$
10. ${\displaystyle i\in [32,33],j\in [-1,1],k\in [0,2]}$
11. ${\displaystyle i\in [0,66],j\in [-1,1],k\in [0,2]}$
12. ${\displaystyle i\in [0,66],j\in [8,24],k\in [0,2]}$
13. ${\displaystyle i\in [8,66],j\in [8,24],k\in [0,2]}$
14. ${\displaystyle i\in [0,23],j\in [8,24],k\in [0,2]}$
15. ${\displaystyle i\in [0,23],j\in [8,24],k\in [0,2]}$
16. ${\displaystyle i\in [0,66],j\in [8,24],k\in [0,2]}$

### C.

${\displaystyle (1,{i\mapsto 0,j\mapsto 0,k\mapsto 0})\cdot (2,{i\mapsto 0,j\mapsto 0,k\mapsto 0})\cdot (3,{i\mapsto 0,j\mapsto 1,k\mapsto 0})\cdot (4,{i\mapsto 0,j\mapsto -1,k\mapsto 0})\cdot (5,{i\mapsto 0,j\mapsto -1,k\mapsto 2})\cdot ...}$

Dass so ein Pfad existiert, bedeutet, dass die Funktion über-approximiert wird.

### D.

i = 0;
while (i < 16)
{ skip;
i = i + 1;
}


Mit der Interval-Analysis erweitern wir nach 4 Schritten, so dass wir am Ende ${\displaystyle i\in [0,\infty ]}$ erhalten, während wir mit der Domain ${\displaystyle L^{i}i\in [0,16]}$ erhalten, da wir nie erweitern müssen, da wir beim zweiten Schritt schon bei ${\displaystyle i\in [0,16]}$angelangen.

## Task 5 - Pointer Analysis and Symbolic Execution

### A. flow-insensitive Pointer Analysis

${\displaystyle r1\mapsto \{A2\}}$, ${\displaystyle r2\mapsto \{A3\}}$, ${\displaystyle s1\mapsto \{A4\}}$, ${\displaystyle s2\mapsto \{A5\}}$, ${\displaystyle p\mapsto \{A2,A3\}}$, ${\displaystyle q\mapsto \{A2,A3\}}$, ${\displaystyle A2.f\mapsto \{A4,A5\}}$, ${\displaystyle A3.f\mapsto \{A4,A5\}}$

### B. flow-sensitive Pointer Analysis

${\displaystyle r1\mapsto \{A2\}}$, ${\displaystyle r2\mapsto \{A3\}}$, ${\displaystyle s1\mapsto \{A4\}}$, ${\displaystyle s2\mapsto \{A5\}}$, ${\displaystyle p\mapsto \{A2,A3\}}$, ${\displaystyle q\mapsto \{A2,A3\}}$, ${\displaystyle A2.f\mapsto \{A4,A5\}}$, ${\displaystyle A3.f\mapsto \{A4,A5\}}$

### C. Symbolic Execution

${\displaystyle \sigma _{s1}:x\mapsto x_{0},y\mapsto y_{0},z\mapsto z_{0},t\mapsto x_{0},w\mapsto x_{0}}$ ${\displaystyle pct_{1}:x_{0}

${\displaystyle \sigma _{s3}:x\mapsto x_{0},y\mapsto y_{0},z\mapsto z_{0},t\mapsto x_{0},w\mapsto z_{0}}$ ${\displaystyle pct_{3}:x_{0}

${\displaystyle \sigma _{s4}:x\mapsto x_{0},y\mapsto y_{0},z\mapsto z_{0},t\mapsto y_{0},w\mapsto y_{0}}$ ${\displaystyle pct_{4}:x_{0}\geq y_{0}\wedge y_{0}

${\displaystyle \sigma _{s5}:x\mapsto x_{0},y\mapsto y_{0},z\mapsto z_{0},t\mapsto y_{0},w\mapsto z_{0}}$ ${\displaystyle pct_{5}:x_{0}\geq y_{0}\wedge y_{0}\geq z_{0}\wedge z_{0}\leq x_{0}}$

### D. pct decidable

The path constraint is important because it tells us under what conditions we can reach a certain program point. If this is not decidable, we do not gain anything out of the analysis because we don't know if and how to reach a certain program point.

### E. simplify pct

• Use rules of boolean algebra (e.g. ${\displaystyle a\wedge b\wedge \neg a}$ can be simplified to ${\displaystyle False}$)
• Use rules of integer arithmetics (e.g. ${\displaystyle x>5\wedge x>3}$ we can simplify that to ${\displaystyle x>5}$)
• Concolic execution can be used to work around unsolvable path constraints through replacing variables with values from a concrete execution.
• maybe more ;-)