Contents

• Introduction
• Programs and procedures
  • Procedures
  • Macros and instructions
  • Inline parameters and recursive macros
  • Ghost variables and ghost code
  • Global variable aliases
  • Modules and includes
• Types, functions, and expressions
  • Types
  • Operands and operand types
  • Functions and consts
  • Expressions
• Complete Vale syntax
  • Grammar
  • Verbatim blocks
  • Lexical structure
  • Attributes
  • Coding conventions
• Using the Vale tool
• Interface with verification framework
  • Vale-generated code
  • Instructions
  • Vale libraries