Documentation for CVC

• 1 Running CVC
  • 1.1 Starting CVC
  • 1.2 Running CVC on the examples
  • 1.3 Command-line options
• 2 Examples
  • 2.1 uninterpreted.cvc
  • 2.2 arrays.cvc
  • 2.3 records.cvc
  • 2.4 adts.cvc
  • 2.5 contexts.cvc
  • 2.6 proofs.cvc
• 3 CVC's presentation language
  • 3.1 Commands
    • 3.1.1 Type declarations
    • 3.1.2 Type definitions
    • 3.1.3 Constant declarations
    • 3.1.4 Constant definitions
    • 3.1.5 ASSERT
    • 3.1.6 QUERY
    • 3.1.7 TRANSFORM
    • 3.1.8 PRINT
    • 3.1.9 ECHO
    • 3.1.10 INCLUDE
    • 3.1.11 WHERE
    • 3.1.12 TRACE
    • 3.1.13 DUMP_PROOF and DUMP_SIG
    • 3.1.14 DUMP_ASSUMPTIONS
    • 3.1.15 PUSH, POP, POPTO, RESET, and CONTEXT
  • 3.2 Types
    • 3.2.1 Basic types
    • 3.2.2 Tuple types
    • 3.2.3 Function types
    • 3.2.4 Record types
    • 3.2.5 Inductive datatypes and scalar types
    • 3.2.6 Array types
  • 3.3 Terms and formulas
    • 3.3.1 Propositional combinations (AND, OR, NOT, XOR, =>, <=>)
    • 3.3.2 Equalities and disequalities (=, /=)
    • 3.3.3 Arithmetic inequalities (<, <=, >, >=)
    • 3.3.4 Tuples
    • 3.3.5 Function applications
    • 3.3.6 Records
    • 3.3.7 Arithmetic operations
    • 3.3.8 IF-THEN-ELSE-ENDIF
    • 3.3.9 LET
    • 3.3.10 WITH
• 4 Semantic notes
  • 4.1 Arithmetic fragment
  • 4.2 Partiality
• 5 Checking proofs with flea