Changeset 1866 for Deliverables


Ignore:
Timestamp:
Mar 15, 2012, 5:28:55 PM (8 years ago)
Author:
campbell
Message:

Drop "extra detail" from WP3.

Location:
Deliverables/D1.2/Presentations
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP3.tex

    r1863 r1866  
    606606}
    607607
    608 \frame{
    609 \frametitle{Extra detail beyond here...}
    610 }
    611 
    612 \begin{frame}[fragile]
    613 \frametitle{Invariants in Cminor}
    614 
    615 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    616 let rec stmt_P (P:stmt $\rightarrow$ Prop) (s:stmt) on s : Prop ≝
    617 match s with
    618 [ St_seq s1 s2 $\Rightarrow$ P s $\wedge$ stmt_P P s1 $\wedge$ stmt_P P s2
    619 | St_ifthenelse _ _ _ s1 s2 $\Rightarrow$ P s $\wedge$ stmt_P P s1 $\wedge$ stmt_P P s2
    620 | St_loop s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
    621 | St_block s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
    622 | St_label _ s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
    623 | St_cost _ s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
    624 | _ $\Rightarrow$ P s
    625 ].
    626 \end{lstlisting}
    627 
    628 Higher order predicate
    629 \begin{itemize}
    630 \item When we pattern match on the statement the predicate can unfold
    631 \item Easy to discharge proof obligations for substatements
    632 \item similar definition for expressions
    633 \end{itemize}
    634 
    635 \end{frame}
    636608\end{document}
Note: See TracChangeset for help on using the changeset viewer.