Skip to content

Commit 8f97736

Browse files
author
Pramod
committed
adding tutorial pdf.
1 parent a4c4f39 commit 8f97736

File tree

2 files changed

+42
-38
lines changed

2 files changed

+42
-38
lines changed

‎tutorial/tutorial.pdf‎

275 KB
Binary file not shown.

‎tutorial/tutorial.toc‎

Lines changed: 42 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,43 +1,47 @@
11
\contentsline {chapter}{\numberline {1}Introduction}{5}{chapter.1}
2-
\contentsline {section}{\numberline {1.1}Getting Started: A Simple \textsc {Uclid5}{} Model}{5}{section.1.1}
2+
\contentsline {section}{\numberline {1.1}Getting Started: A Simple {\textsc {Uclid5}}\xspace {} Model}{5}{section.1.1}
33
\contentsline {subsubsection}{\nonumberline The System Model}{6}{section*.3}
44
\contentsline {subsubsection}{\nonumberline The System Specification}{6}{section*.4}
5-
\contentsline {subsubsection}{\nonumberline The Proof Script}{6}{section*.5}
6-
\contentsline {section}{\numberline {1.2}Installing \textsc {Uclid5}{}}{7}{section.1.2}
5+
\contentsline {subsubsection}{\nonumberline The Proof Script}{7}{section*.5}
6+
\contentsline {section}{\numberline {1.2}Installing {\textsc {Uclid5}}\xspace {}}{7}{section.1.2}
77
\contentsline {subsection}{\numberline {1.2.1}Prerequisites}{7}{subsection.1.2.1}
88
\contentsline {subsection}{\numberline {1.2.2}Detailed Installation Instructions}{7}{subsection.1.2.2}
9-
\contentsline {subsection}{\numberline {1.2.3}Running \textsc {Uclid5}{}}{8}{subsection.1.2.3}
10-
\contentsline {section}{\numberline {1.3}Looking Forward}{8}{section.1.3}
11-
\contentsline {chapter}{\numberline {2}Basics: Types and Statements}{9}{chapter.2}
12-
\contentsline {section}{\numberline {2.1}Types in \textsc {Uclid5}{}}{9}{section.2.1}
13-
\contentsline {section}{\numberline {2.2}Statements in \textsc {Uclid5}{}}{9}{section.2.2}
14-
\contentsline {subsection}{\numberline {2.2.1}For Loops}{11}{subsection.2.2.1}
15-
\contentsline {subsection}{\numberline {2.2.2}If and Case Statements}{11}{subsection.2.2.2}
16-
\contentsline {subsection}{\numberline {2.2.3}Expressions}{11}{subsection.2.2.3}
17-
\contentsline {section}{\numberline {2.3}Computation/Verification Model}{11}{section.2.3}
18-
\contentsline {subsection}{\numberline {2.3.1}Initialization}{11}{subsection.2.3.1}
19-
\contentsline {subsection}{\numberline {2.3.2}Next State Computation}{11}{subsection.2.3.2}
20-
\contentsline {subsection}{\numberline {2.3.3}Verification}{12}{subsection.2.3.3}
21-
\contentsline {subsection}{\numberline {2.3.4}Running \textsc {Uclid5}{}}{12}{subsection.2.3.4}
22-
\contentsline {chapter}{\numberline {3}Verification Techniques}{13}{chapter.3}
23-
\contentsline {section}{\numberline {3.1}Inductive Proofs}{13}{section.3.1}
24-
\contentsline {subsection}{\numberline {3.1.1}Debugging Counterexamples}{13}{subsection.3.1.1}
25-
\contentsline {subsection}{\numberline {3.1.2}Inductive Proof for the Fibonacci Model}{15}{subsection.3.1.2}
26-
\contentsline {chapter}{\numberline {4}Compositional Reasoning with Modules}{17}{chapter.4}
27-
\contentsline {section}{\numberline {4.1}Common Type Definitions Across Modules}{17}{section.4.1}
28-
\contentsline {section}{\numberline {4.2}Uninterpreted Functions and Types}{17}{section.4.2}
29-
\contentsline {subsection}{\numberline {4.2.1}Uninterpreted Types}{17}{subsection.4.2.1}
30-
\contentsline {subsection}{\numberline {4.2.2}Uninterpreted Functions}{19}{subsection.4.2.2}
31-
\contentsline {section}{\numberline {4.3}Procedure Definition}{19}{section.4.3}
32-
\contentsline {subsection}{\numberline {4.3.1}Procedure Invocation}{19}{subsection.4.3.1}
33-
\contentsline {section}{\numberline {4.4}Module Instantiation and Scheduling}{21}{section.4.4}
34-
\contentsline {subsection}{\numberline {4.4.1}Accessing Instance Variables}{21}{subsection.4.4.1}
35-
\contentsline {section}{\numberline {4.5}Running \textsc {Uclid5}{} On The CPU Model}{21}{section.4.5}
36-
\contentsline {subsection}{\numberline {4.5.1}Exercise: Inductive Proof of CPU model}{21}{subsection.4.5.1}
37-
\contentsline {chapter}{\numberline {A}Appendix: \textsc {Uclid5}{} Grammar}{22}{appendix.A}
38-
\contentsline {section}{\numberline {A.1}Grammar of Modules and Declarations}{22}{section.A.1}
39-
\contentsline {section}{\numberline {A.2}Statement Grammar}{24}{section.A.2}
40-
\contentsline {section}{\numberline {A.3}Expression Grammar}{25}{section.A.3}
41-
\contentsline {section}{\numberline {A.4}Types}{26}{section.A.4}
42-
\contentsline {section}{\numberline {A.5}Control Block}{27}{section.A.5}
43-
\contentsline {section}{\numberline {A.6}Miscellaneous Nonterminals}{27}{section.A.6}
9+
\contentsline {subsection}{\numberline {1.2.3}Running {\textsc {Uclid5}}\xspace {}}{8}{subsection.1.2.3}
10+
\contentsline {section}{\numberline {1.3}Looking Forward}{9}{section.1.3}
11+
\contentsline {chapter}{\numberline {2}Basics: Types and Statements}{10}{chapter.2}
12+
\contentsline {section}{\numberline {2.1}Types in {\textsc {Uclid5}}\xspace {}}{10}{section.2.1}
13+
\contentsline {section}{\numberline {2.2}Statements in {\textsc {Uclid5}}\xspace {}}{10}{section.2.2}
14+
\contentsline {subsection}{\numberline {2.2.1}For Loops}{12}{subsection.2.2.1}
15+
\contentsline {subsection}{\numberline {2.2.2}If and Case Statements}{12}{subsection.2.2.2}
16+
\contentsline {subsection}{\numberline {2.2.3}Expressions}{12}{subsection.2.2.3}
17+
\contentsline {section}{\numberline {2.3}Computation/Verification Model}{12}{section.2.3}
18+
\contentsline {subsection}{\numberline {2.3.1}Initialization}{12}{subsection.2.3.1}
19+
\contentsline {subsection}{\numberline {2.3.2}Next State Computation}{12}{subsection.2.3.2}
20+
\contentsline {subsection}{\numberline {2.3.3}Verification}{13}{subsection.2.3.3}
21+
\contentsline {subsection}{\numberline {2.3.4}Running {\textsc {Uclid5}}\xspace {}}{13}{subsection.2.3.4}
22+
\contentsline {chapter}{\numberline {3}Verification Techniques}{14}{chapter.3}
23+
\contentsline {section}{\numberline {3.1}Inductive Proofs}{14}{section.3.1}
24+
\contentsline {subsection}{\numberline {3.1.1}Debugging Counterexamples}{14}{subsection.3.1.1}
25+
\contentsline {subsection}{\numberline {3.1.2}Inductive Proof for the Fibonacci Model}{16}{subsection.3.1.2}
26+
\contentsline {section}{\numberline {3.2}Bounded Model Checking}{17}{section.3.2}
27+
\contentsline {subsection}{\numberline {3.2.1}Embedded assume and assert statements}{17}{subsection.3.2.1}
28+
\contentsline {subsection}{\numberline {3.2.2}Running {\textsc {Uclid5}}\xspace {}}{18}{subsection.3.2.2}
29+
\contentsline {section}{\numberline {3.3}Future Directions}{19}{section.3.3}
30+
\contentsline {chapter}{\numberline {4}Compositional Modeling and Abstraction}{20}{chapter.4}
31+
\contentsline {section}{\numberline {4.1}Common Type Definitions Across Modules}{20}{section.4.1}
32+
\contentsline {section}{\numberline {4.2}Uninterpreted Functions and Types}{20}{section.4.2}
33+
\contentsline {subsection}{\numberline {4.2.1}Uninterpreted Types}{22}{subsection.4.2.1}
34+
\contentsline {subsection}{\numberline {4.2.2}Uninterpreted Functions}{22}{subsection.4.2.2}
35+
\contentsline {section}{\numberline {4.3}Procedure Definition}{22}{section.4.3}
36+
\contentsline {subsection}{\numberline {4.3.1}Procedure Invocation}{24}{subsection.4.3.1}
37+
\contentsline {section}{\numberline {4.4}Module Instantiation and Scheduling}{24}{section.4.4}
38+
\contentsline {subsection}{\numberline {4.4.1}Accessing Instance Variables}{24}{subsection.4.4.1}
39+
\contentsline {section}{\numberline {4.5}Running {\textsc {Uclid5}}\xspace {}}{24}{section.4.5}
40+
\contentsline {subsection}{\numberline {4.5.1}Exercise: Inductive Proof of CPU model}{24}{subsection.4.5.1}
41+
\contentsline {chapter}{\numberline {A}Appendix: {\textsc {Uclid5}}\xspace {} Grammar}{26}{appendix.A}
42+
\contentsline {section}{\numberline {A.1}Grammar of Modules and Declarations}{26}{section.A.1}
43+
\contentsline {section}{\numberline {A.2}Statement Grammar}{28}{section.A.2}
44+
\contentsline {section}{\numberline {A.3}Expression Grammar}{29}{section.A.3}
45+
\contentsline {section}{\numberline {A.4}Types}{30}{section.A.4}
46+
\contentsline {section}{\numberline {A.5}Control Block}{31}{section.A.5}
47+
\contentsline {section}{\numberline {A.6}Miscellaneous Nonterminals}{31}{section.A.6}

0 commit comments

Comments
 (0)