Contents

• Foreword
• Chapter 1  Quick tutorial
  • 1.1  Principles
  • 1.2  A trivial example
  • 1.3  A less trivial example: Dijkstra’s Dutch flag
  • 1.4  Other features
    • 1.4.1  Assertions
    • 1.4.2  Recursive functions
    • 1.4.3  Exceptions
    • 1.4.4  Unreachable code
    • 1.4.5  Non-deterministic programs
  • 1.5  Tools
    • 1.5.1  Graphical user interface (gwhy)
    • 1.5.2  Graphical user interface (WhyWeb)
    • 1.5.3  Remaining Issues
    • 1.5.4  Calling decision procedures (dp)
    • 1.5.5  Why obfuscator (why-obfuscator)
    • 1.5.6  Why statistics (why-stat)
    • 1.5.7  Caml code generation (why --ocaml)
    • 1.5.8  Why to HTML converter (why2html)
    • 1.5.9  Simplify to Why converter (simplify2why)
  • 1.6  Installation
  • 1.7  Examples
  • 1.8  Verifying C and Java programs
• Chapter 2  Reference manual
  • 2.1  Command line
  • 2.2  Syntax of input files
    • 2.2.1  Lexical conventions
    • 2.2.2  Grammar
  • 2.3  Semantics
    • 2.3.1  Logic
    • 2.3.2  Programs
  • 2.4  Prelude
    • 2.4.1  prelude.why
    • 2.4.2  arrays.why
  • 2.5  Provers specificities
    • 2.5.1  Coq
    • 2.5.2  PVS
• Appendix A  DTD of Why project files
• Index