Specification and Verification of Object-Oriented Software in Research and Education

Explore the principles and methods for specifying and verifying object-oriented software, covering concepts like loop invariants, termination conditions, mutual exclusion, procedures, and more.

• Software Engineering
• Object-Oriented Programming
• Verification
• Loop Invariants
• Procedures

grke696 Follow

Uploaded on Sep 14, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Specification and Verification of Object-Oriented Software K. Rustan M. Leino Research in Software Engineering (RiSE) Microsoft Research, Redmond, WA part 2 International Summer School Marktoberdorf Marktoberdorf, Germany 8 August 2008

2. While loop with loop invariant while E invariant J do S end = assert J; havoc x; assume J; ( assume E; S; assert J; assume false assume E ) check that the loop invariant holds initially fast forward to an arbitrary iteration of the loop check that the loop invariant is maintained by the loop body where x denotes the assignment targets of S

3. wp of while wp( while E invariant J do S end, Q ) = J ( x J E wp(S, J) ) ( x J E Q ) assert J; havoc x; assume J; ( assume E; S; assert J; assume false assume E )

4. wp calculation for while wp(havoc x; assume J; assume E; S; assert J; assume false, Q ) = wp(havoc x; assume J; assume E; S; assert J, false Q ) = wp(havoc x; assume J; assume E; S; assert J, true ) = wp(havoc x; assume J; assume E; S, J true ) = wp(havoc x; assume J; assume E; S, J ) = wp(havoc x; assume J; assume E, wp(S, J) ) = wp(havoc x, assume J, E wp(S, J) ) = wp(havoc x, J (E wp(S, J)) ) = wp(havoc x, J E wp(S, J) ) = ( x J E wp(S, J))

5. Loop termination while E invariant J decreases B do S end = ?

6. Example: Mutual exclusion monitor m { var x; invariant x y; } acquire m release m

7. Procedures A procedure is a user-defined command procedure M(x, y, z) returns (r, s, t) requires P modifies g, h ensures Q

8. Procedure example procedure Inc(n) returns (b) requires 0 n modifies g ensures g = old(g) + n b = (g even)

9. Procedure calls procedure M(x, y, z) returns (r, s, t) requires P modifies g, h ensures Q call a, b, c := M(E, F, G) = x := E; y := F; z := G; assert P ; g0 := g; h0 := h; havoc g, h, r , s , t ; assume Q ; a := r ; b := s ; c := t where x , y , z , r , s , t , g0, h0 are fresh variables P is P with x ,y ,z for x,y,z Q is Q with x ,y ,z ,r ,s ,t ,g0,h0 for x,y,z,r,s,t, old(g), old(h)

10. Procedure implementations procedure M(x, y, z) returns (r, s, t) requires P modifies g, h ensures Q implementation M(x, y, z) returns (r, s, t) is S correct if: assume P; g0 := g; h0 := h; S; assert Q is correct syntactically check that S assigns only to g,h where g0, h0 are fresh variables Q is Q with g0,h0 for old(g), old(h)

11. Translating a source language

12. Translation functions The meaning of source statement S is given by Tr[[ S ]] Tr : source-statement command When defined, the meaning of a source expression E is given by Tr[[ E ]] Tr : source-expression expression In a context permitted to read set of locations R, source expression E is defined when DfR[[ E ]] holds DfR : source-expression boolean expression If R is the universal set, drop the subscript R

13. Example translations Tr[[ x := E ]] = assert Df[[ E ]]; x := Tr[[ E ]]

14. Example translations Tr[[ x := E ]] = assert Df[[ E ]]; x := Tr[[ E ]] DfR[[ E / F ]] = DfR[[ E ]] DfR[[ F ]] Tr[[ F ]] 0 DfR[[ E.x ]] = DfR[[ E ]] Tr[[ E ]] null ( Tr[[ E ]], x ) R DfR[[ E && F ]] = DfR[[ E ]] (Tr[[ E ]] DfR[[ F ]])

15. Object features class C { var x: int; var y: C; } Idea: c.x is modeled as Heap[c, x] Details: var Heap const x const y

16. Object features, with types class C { var x: int; var y: C; } Idea: c.x is modeled as Heap[c, x] Details: type Ref type Field var Heap: Ref Field ? const x: Field const y: Field

17. Object features, with types class C { var x: int; var y: C; } Idea: c.x is modeled as Heap[c, x] Details: type Ref; type Field ; var Heap: . Ref Field ; const x: Field int; const y: Field Ref; Heap[c, x] has type int

18. Object features class C { var x: int; var y: C; } Translation into Boogie: type Ref; type Field ; type HeapType = [ Ref, Field ] ; var Heap: HeapType; const unique C.x: Field int; const unique C.y: Field Ref;

19. Accessing the heap introduce: const null: Ref; DfR[[ E.x ]] = DfR[[ E ]] Tr[[ E ]] null ( Tr[[ E ]], x ) R Tr[[ E.x := F ]] = assert Df[[ E ]] Df[[ F ]] Tr[[ E ]] null; Heap[ Tr[[ E ]], x ] := Tr[[ F ]]

20. Object creation introduce: const unique alloc: Field bool; Tr[[ c := new C ]] = havoc c; assume c null Heap[c, alloc]; Heap[c, alloc] := true

21. Object creation, advanced introduce: const unique alloc: Field bool; Tr[[ c := new C ]] = havoc c; assume c null Heap[c, alloc]; assume dtype(c) = C; assume Heap[c, x] = 0 Heap[c, y] = null; Heap[c, alloc] := true dynamic type information initial field values

22. Fresh DfR[[ fresh(S) ]] = DfR[[ S ]] Tr[[ fresh(S) ]] = ( o o Tr[[ S ]] o = null old(Heap)[o, alloc])

23. Properties of the heap introduce: axiom ( h: HeapType, o: Ref, f: Field Ref o null h[o, alloc] h[o, f] = null h[ h[o,f], alloc ] );

24. Properties of the heap introduce: function IsHeap(HeapType) returns (bool); introduce: axiom ( h: HeapType, o: Ref, f: Field Ref IsHeap(h) o null h[o, alloc] h[o, f] = null h[ h[o,f], alloc ] ); introduce: assume IsHeap(Heap) after each Heap update; for example: Tr[[ E.x := F ]] = assert ; Heap[ ] := ; assume IsHeap(Heap)

25. Demo Example0.dfy