Download Bound-T User Manual - Bound

5.10
5.11
5.12
5.13
5.14
5.15
5.16
5.17
5.18
6
THE BOUND-T COMMAND LINE
6.1
6.2
6.3
6.4
6.5
6.6
7
9
10
129
Introduction.................................................................................................129
Assertion Syntax Basics...............................................................................129
Scopes.........................................................................................................132
Global Bounds.............................................................................................133
Subprograms...............................................................................................133
Loops...........................................................................................................135
Calls.............................................................................................................137
Clauses and Facts........................................................................................138
Execution Time Bounds...............................................................................139
Repetition Bounds.......................................................................................140
Variable Bounds...........................................................................................145
Variable Invariance......................................................................................147
Property Bounds..........................................................................................148
Callee Bounds..............................................................................................149
Combining Assertions..................................................................................149
Error Messages from the Assertion Parser...................................................152
TROUBLESHOOTING
9.1
9.2
102
Choice of Outputs........................................................................................102
Basic Output Format....................................................................................102
List of Unbounded Program Parts................................................................108
Tabular Output.............................................................................................110
Detailed Output...........................................................................................115
DOT Drawings..............................................................................................124
ASSERTION LANGUAGE SYNTAX AND MEANING
8.1
8.2
8.3
8.4
8.5
8.6
8.7
8.8
8.9
8.10
8.11
8.12
8.13
8.14
8.15
8.16
79
Basic Form.....................................................................................................79
Special Forms................................................................................................79
Options Grouped by Function........................................................................80
Options in Alphabetic Order..........................................................................83
Optional Analysis Parts..................................................................................96
Patch files....................................................................................................100
UNDERSTANDING BOUND-T OUTPUTS
7.1
7.2
7.3
7.4
7.5
7.6
8
Assertions on Properties................................................................................56
Special Assertions on Subprograms..............................................................57
Scopes and Qualified Names.........................................................................59
Naming Subprograms....................................................................................60
Naming Variables...........................................................................................61
Identifying Loops...........................................................................................62
Identifying Calls.............................................................................................69
Handling Eternal Loops..................................................................................72
Handling Recursion........................................................................................74
157
Bound-T Warning Messages.........................................................................157
Bound-T Error Messages..............................................................................168
GLOSSARY
180
v