VOOZH about

URL: https://www.cs.cmu.edu/~kbierhof/thesis/bierhoff-thesis.pdf

⇱

%PDF-1.4 %���� 5 0 obj << /S /GoTo /D (chapter.1) >> endobj 8 0 obj (1 Introduction) endobj 9 0 obj << /S /GoTo /D (section.1.1) >> endobj 12 0 obj (1.1 APIs and Object Protocols) endobj 13 0 obj << /S /GoTo /D (subsection.1.1.1) >> endobj 16 0 obj (1.1.1 Helping Developers) endobj 17 0 obj << /S /GoTo /D (subsection.1.1.2) >> endobj 20 0 obj (1.1.2 Challenges) endobj 21 0 obj << /S /GoTo /D (section.1.2) >> endobj 24 0 obj (1.2 This Dissertation) endobj 25 0 obj << /S /GoTo /D (subsection.1.2.1) >> endobj 28 0 obj (1.2.1 Expressiveness) endobj 29 0 obj << /S /GoTo /D (subsection.1.2.2) >> endobj 32 0 obj (1.2.2 Subtyping and Inheritance) endobj 33 0 obj << /S /GoTo /D (subsection.1.2.3) >> endobj 36 0 obj (1.2.3 Aliasing Flexibility) endobj 37 0 obj << /S /GoTo /D (subsection.1.2.4) >> endobj 40 0 obj (1.2.4 Contributions) endobj 41 0 obj << /S /GoTo /D (section.1.3) >> endobj 44 0 obj (1.3 Potential Impact) endobj 45 0 obj << /S /GoTo /D (section.1.4) >> endobj 48 0 obj (1.4 Thesis Outline) endobj 49 0 obj << /S /GoTo /D (chapter.2) >> endobj 52 0 obj (2 Thesis and Hypotheses) endobj 53 0 obj << /S /GoTo /D (section.2.1) >> endobj 56 0 obj (2.1 Thesis) endobj 57 0 obj << /S /GoTo /D (section.2.2) >> endobj 60 0 obj (2.2 Hypotheses) endobj 61 0 obj << /S /GoTo /D (subsection.2.2.1) >> endobj 64 0 obj (2.2.1 Capture Common Protocols Succinctly) endobj 65 0 obj << /S /GoTo /D (subsection.2.2.2) >> endobj 68 0 obj (2.2.2 Sound Modular Checking) endobj 69 0 obj << /S /GoTo /D (subsection.2.2.3) >> endobj 72 0 obj (2.2.3 Automation) endobj 73 0 obj << /S /GoTo /D (subsection.2.2.4) >> endobj 76 0 obj (2.2.4 Practical Checking) endobj 77 0 obj << /S /GoTo /D (chapter.3) >> endobj 80 0 obj (3 Approach: Access Permissions) endobj 81 0 obj << /S /GoTo /D (section.3.1) >> endobj 84 0 obj (3.1 Java Iterators) endobj 85 0 obj << /S /GoTo /D (subsection.3.1.1) >> endobj 88 0 obj (3.1.1 Specification Goals) endobj 89 0 obj << /S /GoTo /D (subsection.3.1.2) >> endobj 92 0 obj (3.1.2 State Machine Protocol) endobj 93 0 obj << /S /GoTo /D (subsection.3.1.3) >> endobj 96 0 obj (3.1.3 Iterator Interface Specification) endobj 97 0 obj << /S /GoTo /D (subsection.3.1.4) >> endobj 100 0 obj (3.1.4 Creating and Disposing Iterators) endobj 101 0 obj << /S /GoTo /D (subsection.3.1.5) >> endobj 104 0 obj (3.1.5 Client Verification) endobj 105 0 obj << /S /GoTo /D (subsection.3.1.6) >> endobj 108 0 obj (3.1.6 Modifying Iterators) endobj 109 0 obj << /S /GoTo /D (section.3.2) >> endobj 112 0 obj (3.2 Java Stream Implementations) endobj 113 0 obj << /S /GoTo /D (subsection.3.2.1) >> endobj 116 0 obj (3.2.1 Stream Pipes) endobj 117 0 obj << /S /GoTo /D (subsection.3.2.2) >> endobj 120 0 obj (3.2.2 Buffered Input Streams) endobj 121 0 obj << /S /GoTo /D (section.3.3) >> endobj 124 0 obj (3.3 Summary) endobj 125 0 obj << /S /GoTo /D (chapter.4) >> endobj 128 0 obj (4 Type System) endobj 129 0 obj << /S /GoTo /D (section.4.1) >> endobj 132 0 obj (4.1 Formal Language) endobj 133 0 obj << /S /GoTo /D (subsection.4.1.1) >> endobj 136 0 obj (4.1.1 Syntax) endobj 137 0 obj << /S /GoTo /D (subsection.4.1.2) >> endobj 140 0 obj (4.1.2 State Spaces) endobj 141 0 obj << /S /GoTo /D (subsection.4.1.3) >> endobj 144 0 obj (4.1.3 Access Permissions) endobj 145 0 obj << /S /GoTo /D (subsection.4.1.4) >> endobj 148 0 obj (4.1.4 Permission-Based Specifications) endobj 149 0 obj << /S /GoTo /D (subsection.4.1.5) >> endobj 152 0 obj (4.1.5 Handling Inheritance) endobj 153 0 obj << /S /GoTo /D (subsection.4.1.6) >> endobj 156 0 obj (4.1.6 Behavioral Subtyping) endobj 157 0 obj << /S /GoTo /D (section.4.2) >> endobj 160 0 obj (4.2 Modular Typestate Verification) endobj 161 0 obj << /S /GoTo /D (subsection.4.2.1) >> endobj 164 0 obj (4.2.1 Permission Tracking) endobj 165 0 obj << /S /GoTo /D (subsection.4.2.2) >> endobj 168 0 obj (4.2.2 Packing and Unpacking) endobj 169 0 obj << /S /GoTo /D (subsection.4.2.3) >> endobj 172 0 obj (4.2.3 Calling Methods) endobj 173 0 obj << /S /GoTo /D (subsection.4.2.4) >> endobj 176 0 obj (4.2.4 Field Assignments) endobj 177 0 obj << /S /GoTo /D (subsection.4.2.5) >> endobj 180 0 obj (4.2.5 Permission Reasoning with Splitting and Joining) endobj 181 0 obj << /S /GoTo /D (subsection.4.2.6) >> endobj 184 0 obj (4.2.6 Soundness) endobj 185 0 obj << /S /GoTo /D (subsection.4.2.7) >> endobj 188 0 obj (4.2.7 Example) endobj 189 0 obj << /S /GoTo /D (chapter.5) >> endobj 192 0 obj (5 Polymorphic Permission Inference) endobj 193 0 obj << /S /GoTo /D (section.5.1) >> endobj 196 0 obj (5.1 Inference System) endobj 197 0 obj << /S /GoTo /D (subsection.5.1.1) >> endobj 200 0 obj (5.1.1 Syntax) endobj 201 0 obj << /S /GoTo /D (subsection.5.1.2) >> endobj 204 0 obj (5.1.2 Typechecking Rules) endobj 205 0 obj << /S /GoTo /D (subsection.5.1.3) >> endobj 208 0 obj (5.1.3 Proof Rules) endobj 209 0 obj << /S /GoTo /D (subsection.5.1.4) >> endobj 212 0 obj (5.1.4 Soundness and Completeness) endobj 213 0 obj << /S /GoTo /D (section.5.2) >> endobj 216 0 obj (5.2 Solving Constraints) endobj 217 0 obj << /S /GoTo /D (subsection.5.2.1) >> endobj 220 0 obj (5.2.1 Checking Method Definitions) endobj 221 0 obj << /S /GoTo /D (subsection.5.2.2) >> endobj 224 0 obj (5.2.2 Constraint Satisfiability) endobj 225 0 obj << /S /GoTo /D (chapter.6) >> endobj 228 0 obj (6 Plural: Java Tooling) endobj 229 0 obj << /S /GoTo /D (section.6.1) >> endobj 232 0 obj (6.1 Developer Annotations) endobj 233 0 obj << /S /GoTo /D (section.6.2) >> endobj 236 0 obj (6.2 Background) endobj 237 0 obj << /S /GoTo /D (subsection.6.2.1) >> endobj 240 0 obj (6.2.1 Eclipse) endobj 241 0 obj << /S /GoTo /D (subsection.6.2.2) >> endobj 244 0 obj (6.2.2 Crystal) endobj 245 0 obj << /S /GoTo /D (section.6.3) >> endobj 248 0 obj (6.3 Flow Analysis for Local Permission Inference) endobj 249 0 obj << /S /GoTo /D (subsection.6.3.1) >> endobj 252 0 obj (6.3.1 Annotations Make Analysis Modular) endobj 253 0 obj << /S /GoTo /D (subsection.6.3.2) >> endobj 256 0 obj (6.3.2 Tuple Lattice) endobj 257 0 obj << /S /GoTo /D (subsection.6.3.3) >> endobj 260 0 obj (6.3.3 Comparing and Joining Permission Tuples) endobj 261 0 obj << /S /GoTo /D (subsection.6.3.4) >> endobj 264 0 obj (6.3.4 Composing Tuples) endobj 265 0 obj << /S /GoTo /D (subsection.6.3.5) >> endobj 268 0 obj (6.3.5 Local Must Alias Analysis) endobj 269 0 obj << /S /GoTo /D (subsection.6.3.6) >> endobj 272 0 obj (6.3.6 Dynamic State Tests) endobj 273 0 obj << /S /GoTo /D (subsection.6.3.7) >> endobj 276 0 obj (6.3.7 API Implementation Checking) endobj 277 0 obj << /S /GoTo /D (subsection.6.3.8) >> endobj 280 0 obj (6.3.8 Error Reporting) endobj 281 0 obj << /S /GoTo /D (section.6.4) >> endobj 284 0 obj (6.4 Extensions) endobj 285 0 obj << /S /GoTo /D (subsection.6.4.1) >> endobj 288 0 obj (6.4.1 Immutable Permissions) endobj 289 0 obj << /S /GoTo /D (subsection.6.4.2) >> endobj 292 0 obj (6.4.2 Borrowing) endobj 293 0 obj << /S /GoTo /D (subsection.6.4.3) >> endobj 296 0 obj (6.4.3 Method Cases) endobj 297 0 obj << /S /GoTo /D (subsection.6.4.4) >> endobj 300 0 obj (6.4.4 Marker States) endobj 301 0 obj << /S /GoTo /D (subsection.6.4.5) >> endobj 304 0 obj (6.4.5 Dependent Objects) endobj 305 0 obj << /S /GoTo /D (subsection.6.4.6) >> endobj 308 0 obj (6.4.6 Concrete Predicates) endobj 309 0 obj << /S /GoTo /D (subsection.6.4.7) >> endobj 312 0 obj (6.4.7 Permissions Allowing Dispatch And Field Access) endobj 313 0 obj << /S /GoTo /D (section.6.5) >> endobj 316 0 obj (6.5 Dealing with Java) endobj 317 0 obj << /S /GoTo /D (subsection.6.5.1) >> endobj 320 0 obj (6.5.1 Constructors) endobj 321 0 obj << /S /GoTo /D (subsection.6.5.2) >> endobj 324 0 obj (6.5.2 Private Methods) endobj 325 0 obj << /S /GoTo /D (subsection.6.5.3) >> endobj 328 0 obj (6.5.3 Static Fields \(Globals\) ) endobj 329 0 obj << /S /GoTo /D (subsection.6.5.4) >> endobj 332 0 obj (6.5.4 Arrays) endobj 333 0 obj << /S /GoTo /D (subsection.6.5.5) >> endobj 336 0 obj (6.5.5 Future Work) endobj 337 0 obj << /S /GoTo /D (section.6.6) >> endobj 340 0 obj (6.6 Use Cases) endobj 341 0 obj << /S /GoTo /D (chapter.7) >> endobj 344 0 obj (7 Evaluation) endobj 345 0 obj << /S /GoTo /D (section.7.1) >> endobj 348 0 obj (7.1 Specifying APIs) endobj 349 0 obj << /S /GoTo /D (subsection.7.1.1) >> endobj 352 0 obj (7.1.1 Java Database Connectivity) endobj 353 0 obj << /S /GoTo /D (subsection.7.1.2) >> endobj 356 0 obj (7.1.2 Java Collections Framework) endobj 357 0 obj << /S /GoTo /D (subsection.7.1.3) >> endobj 360 0 obj (7.1.3 Other Java Standard Libraries) endobj 361 0 obj << /S /GoTo /D (section.7.2) >> endobj 364 0 obj (7.2 Beehive: Verifying an Intermediary Library) endobj 365 0 obj << /S /GoTo /D (subsection.7.2.1) >> endobj 368 0 obj (7.2.1 Checked Java Standard Library APIs) endobj 369 0 obj << /S /GoTo /D (subsection.7.2.2) >> endobj 372 0 obj (7.2.2 Implementing an Iterator) endobj 373 0 obj << /S /GoTo /D (subsection.7.2.3) >> endobj 376 0 obj (7.2.3 Formalizing Beehive Client Obligations) endobj 377 0 obj << /S /GoTo /D (subsection.7.2.4) >> endobj 380 0 obj (7.2.4 Overhead: Annotations in Beehive) endobj 381 0 obj << /S /GoTo /D (subsection.7.2.5) >> endobj 384 0 obj (7.2.5 Analysis Precision) endobj 385 0 obj << /S /GoTo /D (section.7.3) >> endobj 388 0 obj (7.3 Iterators in PMD: Scalability and Precision) endobj 389 0 obj << /S /GoTo /D (subsection.7.3.1) >> endobj 392 0 obj (7.3.1 Iterator Usage Protocol) endobj 393 0 obj << /S /GoTo /D (subsection.7.3.2) >> endobj 396 0 obj (7.3.2 Concurrent Modifications) endobj 397 0 obj << /S /GoTo /D (subsection.7.3.3) >> endobj 400 0 obj (7.3.3 Comparison to Tracematches) endobj 401 0 obj << /S /GoTo /D (section.7.4) >> endobj 404 0 obj (7.4 Discussion: Lessons Learned) endobj 405 0 obj << /S /GoTo /D (subsection.7.4.1) >> endobj 408 0 obj (7.4.1 APIs) endobj 409 0 obj << /S /GoTo /D (subsection.7.4.2) >> endobj 412 0 obj (7.4.2 API Client Code) endobj 413 0 obj << /S /GoTo /D (subsection.7.4.3) >> endobj 416 0 obj (7.4.3 Plural Tool Usage) endobj 417 0 obj << /S /GoTo /D (chapter.8) >> endobj 420 0 obj (8 Related Work) endobj 421 0 obj << /S /GoTo /D (section.8.1) >> endobj 424 0 obj (8.1 Static Protocol Analyses) endobj 425 0 obj << /S /GoTo /D (subsection.8.1.1) >> endobj 428 0 obj (8.1.1 Modular Analyses) endobj 429 0 obj << /S /GoTo /D (subsection.8.1.2) >> endobj 432 0 obj (8.1.2 Whole-Program Analyses) endobj 433 0 obj << /S /GoTo /D (section.8.2) >> endobj 436 0 obj (8.2 Protocols at Runtime) endobj 437 0 obj << /S /GoTo /D (section.8.3) >> endobj 440 0 obj (8.3 Verifying Component Compositions) endobj 441 0 obj << /S /GoTo /D (section.8.4) >> endobj 444 0 obj (8.4 Fractional Permission Inference) endobj 445 0 obj << /S /GoTo /D (section.8.5) >> endobj 448 0 obj (8.5 Comprehensive Program Verification) endobj 449 0 obj << /S /GoTo /D (section.8.6) >> endobj 452 0 obj (8.6 Protocol Inference) endobj 453 0 obj << /S /GoTo /D (chapter.9) >> endobj 456 0 obj (9 Conclusions) endobj 457 0 obj << /S /GoTo /D (section.9.1) >> endobj 460 0 obj (9.1 Validation of Hypotheses) endobj 461 0 obj << /S /GoTo /D (subsection.9.1.1) >> endobj 464 0 obj (9.1.1 Capture Common Protocols Succinctly) endobj 465 0 obj << /S /GoTo /D (subsection.9.1.2) >> endobj 468 0 obj (9.1.2 Sound Modular Checking) endobj 469 0 obj << /S /GoTo /D (subsection.9.1.3) >> endobj 472 0 obj (9.1.3 Automation) endobj 473 0 obj << /S /GoTo /D (subsection.9.1.4) >> endobj 476 0 obj (9.1.4 Practical Checking) endobj 477 0 obj << /S /GoTo /D (subsection.9.1.5) >> endobj 480 0 obj (9.1.5 Thesis) endobj 481 0 obj << /S /GoTo /D (section.9.2) >> endobj 484 0 obj (9.2 Concerns) endobj 485 0 obj << /S /GoTo /D (subsection.9.2.1) >> endobj 488 0 obj (9.2.1 Variations in Development Practices) endobj 489 0 obj << /S /GoTo /D (subsection.9.2.2) >> endobj 492 0 obj (9.2.2 Applicability to Frameworks) endobj 493 0 obj << /S /GoTo /D (subsection.9.2.3) >> endobj 496 0 obj (9.2.3 Expression Cost) endobj 497 0 obj << /S /GoTo /D (subsection.9.2.4) >> endobj 500 0 obj (9.2.4 Adoptability) endobj 501 0 obj << /S /GoTo /D (subsection.9.2.5) >> endobj 504 0 obj (9.2.5 Tool Performance) endobj 505 0 obj << /S /GoTo /D (subsection.9.2.6) >> endobj 508 0 obj (9.2.6 Concurrency) endobj 509 0 obj << /S /GoTo /D (section.9.3) >> endobj 512 0 obj (9.3 Discussion) endobj 513 0 obj << /S /GoTo /D (subsection.9.3.1) >> endobj 516 0 obj (9.3.1 Pay-off and Incrementality) endobj 517 0 obj << /S /GoTo /D (subsection.9.3.2) >> endobj 520 0 obj (9.3.2 Essential Features) endobj 521 0 obj << /S /GoTo /D (subsection.9.3.3) >> endobj 524 0 obj (9.3.3 Advice to API Designers) endobj 525 0 obj << /S /GoTo /D (subsection.9.3.4) >> endobj 528 0 obj (9.3.4 Effect on Software Engineering Practice) endobj 529 0 obj << /S /GoTo /D (section.9.4) >> endobj 532 0 obj (9.4 Contributions) endobj 533 0 obj << /S /GoTo /D (section.9.5) >> endobj 536 0 obj (9.5 Future Work) endobj 537 0 obj << /S /GoTo /D (section.9.6) >> endobj 540 0 obj (9.6 Summary) endobj 541 0 obj << /S /GoTo /D [542 0 R /Fit ] >> endobj 544 0 obj << /Length 1188 /Filter /FlateDecode >> stream xڍV�r�6��+X5�j�`�G�'��m�i��h���  =�ߧ�P���\H������M�`������/�\�4 bIF��U@X�ɂ ��,A����:�i�å�H�Q��w��|���Z�~��������)���wNX�����>x��÷�P �Y�E����$ _go_W�Z�K�1 F%.��8A9˂8IPV��)s���>Q�qicƄ���f(MJwa�`sc�����}��y$��YIȑ�0�ޠ U&(! D����|=�Q����[Iu�UDp�(���7���*RĊ򴆺�ȹ-ruh��}�Ѝ�C�����Ш��>� �{�{�8ӘWc�����������R��~�('�����OTҰrg�R���q��a�2-!��