Type Systems for Security Verification Lecture
Saarland University
Tuesday, 17 March 2015
1st Homework
Extending project period to Monday, 30 March
Lemma t (requires r) (ensures e) = Pure unit (requires r) (ensures (fun _ -> e))
Tot t = Pure (requires True) (ensures True)
Semantic termination checking
Simple effects: non-termination, exceptions
Examples
Tutorial
e1 << e2
(e1
precedes e2
)
(<<) : #a:Type -> #b:Type -> a -> b -> Type
e1 >> e2 >> ...
)
(decreases ...)
clause
i, j : nat
then i << j <==> i < j
.
<<
hd::tl << hd
and hd::tl << tl
lex_t
are ordered lexicographically
type lex_t = LexTop : lex_t | LexCons: #a:Type -> a -> lex_t -> lex_t
%[v1;...;vn]@ = LexCons v1 ... (LexCons vn LexTop)
LexCons v1 v2 << LexCons v1' v2'
if and only ifv1 << v1'
or (v1=v1'
and v2 << v2'
)
v:lex_t
and v \neq LexTop
, then v << LexTop
DIV
arrow)
Same as pure, just no termination check
DIV ~ PURE
, Div ~ Pure
, Dv ~ Tot
Lemma
, of course
val loop : u:unit -> Div unit (requires True) (ensures (fun _ -> False))
let rec loop () = loop ()
We'll see examples soon (While interpreter)
raise
exceptions
try e1 with
| pattern1 -> expression2
| pattern2 -> expression3
...
DIV
actually),EXN ~~ PURE
, Exn ~~ Pure
, Ex ~~ Tot
EXN
includes DIV
(DIV <: EXN
)
if-then-else
removing while
) - 2 x 1p