Transcript Operation - Clemson University

Reasoning with Objects and
Web Interface Demo
Computer Science  School of Computing  Clemson University
Jason Hallstrom and Murali Sitaraman
Clemson University
Example
School of Computing  Clemson University
Specification:
Operation Do_Nothing (restores S: Stack);
Goal: Same as ensures S = #S;
Code: (Same as S.Push(S.Pop()) in Java)
Procedure Do_Nothing (restores S: Stack);
Var E: Entry;
Pop(E, S);
Push(E, S);
end Do_Nothing;
Exercise: Complete table and prove!
School of Computing  Clemson University
Assume
0
Confirm
…
…
…
…
…
…
Pop(E, S);
1
Push(E, S);
2

Don’t yet! Instead of IntStacks, we will use general stacks
for this example reasoning…because verifying reusable,
generic software has more pay-off!
General Stack Template
Specification
School of Computing  Clemson University
 Instead of IntStacks, we will use general
stacks for this example reasoning
 Suppose Stack_Template is
parameterized by type Entry and Integer
Max_Depth
 Mathematical Modeling
 Type Stack is modeled by Str(Entry);
 exemplar S;
 constraints |S| <= Max_Depth;
 initialization ensures S = empty_string;
Specification of Stack Operations
School of Computing  Clemson University
Operation Push (alters E: Entry; updates S: Stack);
requires |S| < Max_Depth;
ensures S = <#E> o #S;
Operation Pop (replaces R: Entry; updates S: Stack);
requires |S| > 0;
ensures #S = <R> o S;
Operation Depth (restores S: Stack): Integer;
ensures Depth = |S|;
…
Collaborative Exercise: Complete
table and prove!
School of Computing  Clemson University
Assume
0
Confirm
…
…
…
…
…
…
Pop(E, S);
1
Push(E, S);
2
Collaborative Exercise: Answers
School of Computing  Clemson University
Assume
0
Confirm
…
|S0| > 0
S0 = <E1> o S1
|S1| < Max_Depth
S2 = <E1> o S1
S2 = S0
Pop(E, S);
1
Push(E, S);
2
…
Discussion
School of Computing  Clemson University
 Can you explain why there are three
confirm assertions?
 Is the code Correct? If not, fix it!
Discussion
School of Computing  Clemson University
 Can you explain why there are three
confirm assertions?
 Is the code Correct? If not, fix it!
 You can either rewrite the code with an
“if” statement or add the following
requires clause to Do_Nothing
operation
 requires |S| > 0;
Key Ideas
School of Computing  Clemson University
 The reasoning table can be filled
mechanically; no intelligence is
required and even a computer can do
it!
 Principles of reasoning about all
objects and operations are the same
 Need mathematical models and
specifications
Automated Reasoning
School of Computing  Clemson University
 The assume and confirm assertions we
wrote out in the table can be
generated automatically
 Each confirm assertion becomes a
“goal”. The assumptions that can be
used to prove that are the “givens”.
 A goal along with the givens is called a
verification condition (VC).
 For the Do_Nothing example, three
VCs need to be proved, because there
are three assertions to be confirmed.
Web Interface Demo
School of Computing  Clemson University
 Google “clemson resolve”
 Click on the web interface link
 Select Stack_Template under Concepts
 Select Do_Nothing_Capability under
the tab Enhancements
 Select Do_Nothing_Realiz under the
Tab Enhancement Realizations
Web Interface Demo
School of Computing  Clemson University
 Click on Generate VCs tab.
 You should see 3 VCs.
 See if you can prove the goals from
the givens! It should be easy…
 Note #1: The VC generator minimizes
the need for new names, such as S1,
S2, S3, etc., so there are less names
and they don’t correspond to states in
the code directly.
 Note #2: VC generator uses S’, S’’,
etc.
Web Interface Help
School of Computing  Clemson University
 Click the Help tab on the right top
corner
 You should see Screencasts. They
illustrate “how to” for various web
interface activities; more use cases
continue to be added.
 You should see Tutorials. The help
learn specific principles; more tutorials
are under development.