JavaCard p.1/41 - PDF 無料ダウンロード

JavaCard Email : nagamiya@comp.cs.gunma-u.ac.jp p.1/41

Hoare Java p.2/41

(formal method) (formal specification) (formal) JML, D, VDM, (formal method) p.3/41

Hoare Java p.4/41

(precondition) (postcondition) p.5/41

Hoare [φ] P [ψ ] φ, ψ P φ P P ψ [φ] P [ψ ] P p.6/41

[ψ[e/x]] x = E [ψ ] ψ[e/x] ψ x E [x + 1 > 1] x = x + 1 [x > 1] p.7/41

[φ] C 1 [η ] [η ] C 2 [ψ ] [φ] C 1 ; C 2 [ψ ] φ C 1 η C 2 ψ p.8/41

AR φ φ [φ] C [ψ ] AR ψ ψ [φ ] C [ψ ] p.9/41

AR 0 = 0 [0 = 0 ] x = 0 [x = 0 ] [ ] x = 0 [x = 0 ] [x = 0 ] y = x [y = 0 ] [ ] x = 0; y = x [y = 0 ] p.10/41

AR 0 = 0 [0 = 0 ] x = 0 [x = 0 ] [ ] x = 0 [x = 0 ] [x = 0 ] y = x [y = 0 ] [ ] x = 0; y = x [y = 0 ] [ ] [0 = 0 ] x = 0; [x = 0 ] y = x; [y = 0 ] p.11/41

if [φ B ] C 1 [ψ ] [φ B ] C 2 [ψ ] [φ] if B {C 1 else {C 2 [ψ ] φ true false φ B B φ B C 1 C 2 ψ p.12/41

while [ψ B ] C [ψ ] [ψ ] while B {C [ψ B ] ψ (loop invariant) ψ ψ B true B false C ψ B p.13/41

y = 1; z = 0; l1: while (z!= x) { z = z + 1; y = y * z; l2: p.14/41

[ ] y = 1; z = 0; l1: while (z!= x) { z = z + 1; y = y * z; l2: [y = x!] p.15/41

x = 6 z at l1 y at l1 z x! at l1 0 0 1 true 1 1 1 true 2 2 2 true 3 3 6 true 4 4 24 true 5 5 120 true 6 6 720 false p.16/41

x = 6 z at l1 y at l1 z x! at l1 0 0 1 true 1 1 1 true 2 2 2 true 3 3 6 true 4 4 24 true 5 5 120 true 6 6 720 false y = z! p.16/41

while [[ ]] y = 1; z = 0; [[y = z!]] l1: while (z!= x) { [[y = z! z x]] z = z + 1; y = y * z; [[y = z!]] l2: [[y = z! z = x]] [[y = x!]] p.17/41

[[ ]] y = 1; z = 0; [[y = z!]] l1: while (z!= x) { [[y = z! z x]] z = z + 1; [[y z = z!]] y = y * z; [[y = z!]] l2: [[y = z! z = x]] [[y = x!]] p.18/41

[[ ]] y = 1; z = 0; [[y = z!]] l1: while (z!= x) { [[y = z! z x]] [[y (z + 1) = (z + 1)!]] z = z + 1; [[y z = z!]] y = y * z; [[y = z!]] l2: [[y = z! z = x]] [[y = x!]] p.19/41

[[ ]] y = 1; [[y = 0!]] z = 0; [[y = z!]] l1: while (z!= x) { [[y = z! z x]] [[y (z + 1) = (z + 1)!]] z = z + 1; [[y z = z!]] y = y * z; [[y = z!]] l2: [[y = z! z = x]] [[y = x!]] p.20/41

[[ ]] [[1 = 0!]] y = 1; [[y = 0!]] z = 0; [[y = z!]] l1: while (z!= x) { [[y = z! z x]] [[y (z + 1) = (z + 1)!]] z = z + 1; [[y z = z!]] y = y * z; [[y = z!]] l2: [[y = z! z = x]] [[y = x!]] p.21/41

[[ ]] [[1 = 0!]] AR 1 = 0! y = 1; [[y = 0!]] z = 0; [[y = z!]] l1: while (z!= x) { [[y = z! z x]] AR (y = z! z x) [[y (z + 1) = (z + 1)!]] (y (z + 1) = (z + 1)!) z = z + 1; [[y z = z!]] y = y * z; [[y = z!]] l2: [[y = z! z = x]] [[y = x!]] AR (y = z! z = x) (y = x!) p.22/41

[[ ]] [[1 = 0!]] AR 1 = 0! y = 1; [[y = 0!]] z = 0; [[y = z!]] Q.E.D l1: while (z!= x) { [[y = z! z x]] AR (y = z! z x) [[y (z + 1) = (z + 1)!]] (y (z + 1) = (z + 1)!) z = z + 1; [[y z = z!]] y = y * z; [[y = z!]] l2: [[y = z! z = x]] [[y = x!]] AR (y = z! z = x) (y = x!) p.23/41

Hoare Java p.24/41

(Design by contract) [φ] P [ψ ] (contract) φ P P ψ φ ψ p.25/41

(precondition) (postcondition) (invariant) p.26/41

Java Modeling Language Java Design by contract p.27/41

JML JML @ //@... /*@... *@... *@/ p.28/41

JML requires ensures //@ requires array.length >=1; //@ ensures \result >= x; invariant //@ public invariant balance >= 0; modefiable //@ modifiable array[x]; p.29/41

JML \result E \old(e) \forall, \exists p.30/41

Krakatoa+Coq Java + JML (Ocaml) proof obligation ( ) Krakatoa Why Coq Krakatoa: Java/JML Why: Hoare proof obligation Coq: proof obligation p.31/41

Krakatoa+Coq Java + JML (Ocaml) proof obligation ( ) Krakatoa Why Coq Krakatoa: Java/JML Why: Hoare proof obligation Coq: proof obligation proof obligation p.31/41

Gemplus JavaCard (ID ) p.32/41

Utils Jour Mois Annee Decimal Pcpcapinterfaces PurseLoyaltyInterface Loyalty TransactionInterface Shareable p.33/41

Decimal 3.493 JavaCard int intpart, decpart short decpart 3 Decimal 0 <= decpart && decpart < PRECISION setvalue intpart = 3 decpart = 493 oppose PRECISION short 1000 sub add mul p.34/41

add private void add(short e, short f) { intpart += e; decpart += f; if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.35/41

add 3.493 Decimal Decimal intpart = 3 intpart = 4 setvalue decpart = 493 oppose setvalue decpart = 507 oppose sub mul add sub mul add intpart * PRECISION + decpart = 3493 p.36/41

add /*@ private normal_behavior @ requires -PRECISION < f && f < PRECISION && @ -MAX_DECIMAL_NUMBER <= e && e <= MAX_DECIMAL_NUMBER && @ -MAX_DECIMAL_NUMBER <= e + intpart - 1 && @ e + intpart + 1 <= MAX_DECIMAL_NUMBER; @ modifiable intpart, decpart; @ ensures intpart * PRECISION + decpart == @ (\old(intpart) + e) * PRECISION + \old(decpart) + f; @*/ private void all (short e, short f) {... p.37/41

add private void add(short e, short f) { intpart += e; decpart += f; intpart PRECISION + decpart = (intpart 0 + e) PRECISION + decpart 0 + f if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

add private void add(short e, short f) { intpart += e; decpart += f; intpart PRECISION + decpart = (intpart 0 + e) PRECISION + decpart 0 + f intpart PRECISION + decpart = (intpart 0 + e) PRECISION + decpart 0 + f if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

add private void add(short e, short f) { intpart += e; decpart += f; intpart PRECISION + decpart = (intpart 0 + e) PRECISION + decpart 0 + f (intpart + 1) PRECISION + decpart = (intpart 0 + e) PRECISION + decpart 0 + f if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

add private void add(short e, short f) { intpart += e; decpart += f; intpart PRECISION + decpart = (intpart 0 + e) PRECISION + decpart 0 + f (intpart + 1) PRECISION +(decpart PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

add (intpart 1) PRECISION + decpart = (intpart 0 + e) PRECISION + decpart 0 + f (intpart + 1) PRECISION +(decpart PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f private void add(short e, short f) { intpart += e; decpart += f; if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

add (intpart 1) PRECISION +(decpart + PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f (intpart + 1) PRECISION +(decpart PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f private void add(short e, short f) { intpart += e; decpart += f; if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

add (decpart PRECISION ) (intpart 1) PRECISION +(decpart + PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f (decpart > PRECISION ) (decpart PRECISION ) (intpart + 1) PRECISION +(decpart PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f private void add(short e, short f) { intpart += e; decpart += f; if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

add (decpart PRECISION ) (intpart 1) PRECISION +(decpart + PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f Q.E.D (decpart > PRECISION ) (decpart PRECISION ) (intpart + 1) PRECISION +(decpart PRECISION ) = (intpart 0 + e) PRECISION + decpart 0 + f private void add(short e, short f) { intpart += e; decpart += f; if (decpart <= -PRECISION) { decpart += PRECISION; intpart--; else if (decpart >= PRECISION) { decpart -= PRECISION; intpart++; p.38/41

Hoare Java p.39/41

: Krakatoa add proof obligation = : mul p.40/41

Thank You! p.41/41