Previous Up

Index

  • arithmetic overflow, 2.2
  • assigns clause, 2.7
  • assigns-clause
    • non-terminal, 3.2
  • \at construct, 2.5

  • behavior, 2.8
  • behavior declaration, 2.8
  • bin-op
    • non-terminal, 3.1
  • binders
    • non-terminal, 3.1
  • built-in-logic-type
    • non-terminal, 3.1


  • Coq, 4.1

  • ensures clause, 2.1
  • ensures-clause
    • non-terminal, 3.2


  • ghost declaration, 2.10
  • ghost variables, 2.10

  • Java, ??, 2.1, 2.6

  • Krakatoa, 2.1
  • krakatoa command, 2.1

  • lexpr
    • non-terminal, 3.1
  • locations
    • non-terminal, 3.2
  • logic predicates, 2.4
  • logic-type-expr
    • non-terminal, 3.1
  • loop invariant, 2.2
  • loop_invariant clause, 2.2
  • loop_variant clause, 2.2

  • \old construct, 2.5

  • postcondition, 2.1
  • precondition, 2.2
  • predicate declaration, 2.4

  • requires clause, 2.2
  • requires-clause
    • non-terminal, 3.2


  • safety, 2.2
  • signals clause, 2.8

  • termination, 2.2
  • type-expr
    • non-terminal, 3.1


  • unary-op
    • non-terminal, 3.1


  • variable-ident
    • non-terminal, 3.1
Previous Up