Logic-Level Syntax

A C* source file contains two languages. Outside backticks, the source text is C, read by the C* compiler. Inside backticks, it is the logic-level language, used in contracts, global proof declarations, and arguments to proof-kernel functions. These logical expressions denote HOL types or HOL terms and are lexed, parsed, and type-checked by HOL Light, the proof assistant on which C* is built.

This language is HOL Light’s, not C’s. Its lexer, precedence table, binders, and type inference come from HOL Light, so a term such as `!n. n > 0i ==> ~(n = 0i)``!n. n > 0i ==> ~(n = 0i)` has exactly the same meaning in C* as in a HOL Light session with the C* extensions loaded. C* extends this language with type constants for verification (hprophprop, ctypectype, struct_namestruct_name, fieldfield) and the abbreviations addraddr and bytebyte, the integer literal suffix ii, the separation-logic connectives, and a naming convention that relates logical variables to program variables.

These reference pages cover both the syntax inherited from HOL Light and the extensions provided by C*.

HOL Light Syntax specifies the inherited syntax: the lexical structure (character classes, identifiers, reserved words, string literals), the type syntax (the TyvarTyvar/TyappTyapp abstract syntax, postfix type application, the ^^, ##, ++, ->-> constructors and their precedence), and the term syntax (the VarVar/ConstConst/CombComb/AbsAbs abstract syntax, the full infix precedence table, term forms such as lists, set comprehensions, matchmatch and letlet, the binders and prefixes, and how type inference resolves overloading and implicit types).

C* Extensions specifies the additions made by C*: the verification-oriented type constants and abbreviations, the 123i123i integer literals, the heap-proposition constants and separation-logic connectives, the typed memory predicates, the ctypectype constants together with sizeofsizeof, min_ofmin_of, max_ofmax_of, and field_addrfield_addr, the fixed-width bitwise operators, the reserved logical variable names (x__addrx__addr, x__prex__pre, __return__return) that the symbolic execution engine uses to refer to program variables, and the catalogue of cst::cst:: attributes used to introduce quotations into a program.