More Related Content
Similar to 「Frama-Cによるソースコード検証」 (mzp)
Similar to 「Frama-Cによるソースコード検証」 (mzp) (20)
More from Hiroki Mizuno (20)
「Frama-Cによるソースコード検証」 (mzp)
- 2. mzp /
SE
> ocaml-nagoya
> ProofCafe
> Scala
2
- 7. @bleis bf SQL
@sunflat Amazon EC2
@yoya PHP: ZendEngine
@terurou CommonJS
@nari3 GC
@mallowlabs AsakusaSattelite
@yoshihiro503 Coq
@mzp
@wof_moriguchi F#
@keigoi ocamljs ocaml android ( )
@osiire GADT
@kaizen_nagoya XYZ
@dico_leque Meta-objective Lisp
6
- 8. @bleis bf SQL
@sunflat Amazon EC2
@yoya PHP: ZendEngine
@terurou CommonJS
@nari3 GC
@mallowlabs AsakusaSattelite
@yoshihiro503 Coq
@mzp !
@wof_moriguchi F#
@keigoi ocamljs ocaml android ( )
@osiire GADT
@kaizen_nagoya XYZ
@dico_leque Meta-objective Lisp
7
- 13. template
≦ OK
> (structual subtype)
template <class T>
T min(T x, T y) {
return (x <= y) ? x : y;
}
12
- 14. auto concept Le<class T> {
bool operator<=(T, T);
}
template <class T> requires Le<T>
T min(T x, T y) {
return x <= y ? x : y;
}
13
- 15. // int
BOOST_CHECK_EQUAL( min(1, 2), 1 );
BOOST_CHECK_EQUAL( min(2, 1), 1 );
BOOST_CHECK_EQUAL( min(3, 3), 3 );
// dobule
BOOST_CHECK_EQUAL( min(1., 2.), 1. );
BOOST_CHECK_EQUAL( min(2., 1.), 1. );
14
- 17. 1
min
≦ OK
template <class T> requires Le<T>
T min3(T x, T y, T z) {
return min(x, min(y, z));
}
16
- 18. // int
BOOST_CHECK_EQUAL( min3(1, 2,3), 1 );
BOOST_CHECK_EQUAL( min3(2, 1,3), 1 );
BOOST_CHECK_EQUAL( min3(3, 2,1), 1 );
// dobule
BOOST_CHECK_EQUAL( min3(1., 2.,4.), 1. );
BOOST_CHECK_EQUAL( min3(2., 1.,4.), 1. );
17
- 20. “ ”: int int
≦ :x≦y z≦w (x,z) ≦
(y,w)
&'( !"#"$
← !"#%$ !%#"$
)*( !%#%$
19
- 21. “ ”: int int
≦ :x≦y z≦w (x,z) ≦
(y,w)
&'( !"#"$
← !"#%$ !%#"$
)*( !%#%$
19
- 22. ≦ OK ←
> :x≦x
> :x≦y y≦z x≦z
↑
20
- 23. > ≦ bool
min,min3
↑
21
- 28. C → Why →
> Alt-Ergo: ←
> Coq: ←
> ...and more
ACSL
> ACSL = ANSI/ISO C Specification Language
!"#$#%& '() *+,%-"./
25
00&/1
- 29. : abs()
abs : 0
ACSL
//@ ensures result >= 0;
int abs (int i) {
return i < 0 ? -i : i;
}
26
- 35. requires
INT_MIN
//@ requires i > -2147483648;
//@ ensures result >= 0;
int abs (int i) {
return i < 0 ? -i : i;
28
- 38. : LE
≦ → LE
>C ACSL
/*@ axiomatic order {
predicate LE(T x, T y);
} */
31
- 39. Frama-C
min,min3 C++ Frama-C
T → void*
→
>
typedef void* T;
bool leq(T x, T y) { return true; }
32
- 40. leq
leq : LE
> leq(x,y) true LE(x,y)
> leq(x,y) false LE(y, x)
/*@ ensures
(¥result == true ==> LE(x,y)) &&
(¥result == false ==> LE(y,x)); */
bool leq(T x, T y){ ... }
33
- 41. min
leq min
x,y
/*@ ensures LE(¥result, x) &&
LE(¥result, y); */
T min(T x,T y){ return leq(x,y) ? x : y; }
34
- 45. min3
min3 : x,y,z
/*@ ensures
LE(result, x) &&
LE(result, y) &&
LE(result, z); */
T min3(T x,T y,T z){
return min(x, min(y,z));
38
- 47. > Coq
→
LE( , min(y,z))
LE(min(y,z), y)
LE( , y)
40
- 48. /*@ axiomatic order {
predicate LE(T x, T y);
axiom refl : ¥forall T x; LE(x,x);
axiom trans: forall T x,T y,T z;
LE(x,y) ==> LE(y,z) ==> LE(x,z);
←
41
Editor's Notes
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
- \n
