<h2>Objects</h2>
- Introduce heap H:\[int\]\[fieldname\]->value
- o.fn = 3 is encoded as H\[0\]\[fieldname\] := 3
<h2>Approach 2 error handling</h2>
\{P\} S_1,S_2 !H \{Q,R\}
- wlp (x=e)(Q,R) = Q\[e/x\]
- wlp **raise** (Q,R) = R
- wlp (S_1;S_2)(Q,R)=wlp S_1 (wlp S_2 (Q,R),R)
- wlp (S ! H)(Q,R) = wlp S (Q,wlp H (Q,R))
<h2>Model checking</h2>
- This pack:
     - Abstract model of programs
     - Temporal properties
     - Verification (via model checking) algorithm
     - Concurrency
    <h3>Run-time properties</h3>
    - Hoare tripple: express what should hold when the program terminates
    - Many programs are supposed to work continuously
         -   The should be safe
         - Not dead lock
         - No starvation
    - LTL (Linear Termporal Logic)
    <h2>FSA</h2>
    - $S$: the set of possible states
    - $I\subseteq S$: Set of possible initial states
    - $\Sigma$: Set of labels, to decorate the arrows
    - $R:S\to \Sigma \to \text{pow}(S)$: Edges
    Program compositions:
    - $M_1;M_2$ 
    - $M_1 \cap M_2$ Intersection
    - $M_1||M_2$ Parralel