Formalized-subset
Subset of the abstract syntax that has a formal semantics.
The C syntax for tools is designed to cover all of C (currently after preprocessing),
but the formal language definition only covers a subset of C.
More precisely:
the abstract syntax of the formal language definition
is a subset of the abstract syntax for tools;
the static semantics of C is defined for
a subset of the latter abstract syntax;
and the dynamic semantics of C is defined for
a subset of the subset for which the static semantics is defined.
Note how these subsets are linearly ordered.
It is useful to characterize which subset of the abstract syntax for tools
corresponds to the subset of C that has both static and dynamic semantics.
This is the subset for which we can state and prove formal properties,
e.g. of a C-to-C transformation. Here we provide such a characterization,
in the form of predicates over the abstract syntax fixtypes.
Note that the subset of the abstract syntax for tools
that corresponds to the abstract syntax of the language definition
is implicitly defined by mapping between the two abstract syntaxes: it is the subset for which the mapping does not return an error.
We could also define separate predicates
over the abstract syntax for tools
that identify the subset with static semantics,
which is between the one defined by
the syntactic language definition mapping
and the one that has dynamic semantics.
However, for now we do not do that,
because that intermediate subset is not particularly interesting:
we are generally more interested in proofs about the dynamic semnantics.
Exactly characterizing the subset with formal dynamic semantics
is not that straightforward, due to the complexity of the constructs.
An exact characterization may also need some type information,
resulting from a static semantic analysis of the code.
The current characterization is a good starting point,
but it needs to be improved.
Subtopics
- Expr-pure-formalp
- Check if an expression has formal dynamic semantics,
as a pure expression.
- Type-spec-list-integer-formalp
- Check if a list of type specifiers has formal dynamic semantics,
when used to denote an integer type.
- Stmts/blocks-formalp
- Chek if statements and blocks have formal dynamic semantics.
- Extdecl-formalp
- Check if an external declaration has dynamic formal semantics.
- Ident-formalp
- Check if an identifier has formal dynamic semantics.
- Type-spec-list-formalp
- Check if a list of type specifiers has formal dynamic semantics.
- Tyname-formalp
- Check if a type name has formal dynamic semantics.
- Pointers-formalp
- Check if a list of pointers has formal dynamic semantics.
- Dirdeclor-obj-formalp
- Check if a direct declarator has formal dynamic semantics,
as part of an object declaration (not in a block).
- Desiniter-formalp
- Check if an initializer with optional designations
has formal dynamic semantics.
- Fundef-formalp
- Check if a function definition has dynamic formal semantics.
- Decl-obj-formalp
- Check if a declaration has formal dynamic semantics,
as an object declaration (not in a block).
- Decl-block-formalp
- Check if a declaration has formal dynamic semantics,
as a block item.
- Initdeclor-obj-formalp
- Check if an initializer declarator has formal dynamic semantics,
as part of an object declaration (not in a block).
- Expr-asg-formalp
- Check if an expression has formal dynamic semantics,
as an assignment expression.
- Structdecl-formalp
- Check if a structure declaration has formal dynamic semantics.
- Initdeclor-block-formalp
- Check if an initializer declarator has formal dynamic semantics,
as part of a block item declaration.
- Decl-struct-formalp
- Check if a declaration has formal dynamic semantics,
as a declaration for a structure type.
- Dirdeclor-fun-formalp
- Check if a direct declarator has formal dynamic semantics,
as part of a function declaration.
- Dirdeclor-block-formalp
- Check if a direct declarator has formal dynamic semantics,
as part of a block item declaration.
- Initdeclor-fun-formalp
- Check if an initializer declarator has formal dynamic semantics,
as part of a function declaration.
- Transunit-ensemble-formalp
- Check if a translation unit ensemble has formal dynamic semantics.
- Param-declor-formalp
- Check if a parameter declarator has formal dynamic semantics.
- Initer-formalp
- Check if an initializer has formal dynamic semantics.
- Expr-call-formalp
- Check if an expression has formal dynamic semantics,
as a call expression.
- Declor-obj-formalp
- Check if a declarator has formal dynamic semantics,
as part of an object declaration (not in a block).
- Decl-fun-formalp
- Check if a declaration has dynamic formal semantics,
as a function declaration.
- Param-declon-formalp
- Check if a parameter declaration has formal dynamic semantics.
- Structdeclor-formalp
- Check if a structure declarator has formal dynamic semantics.
- Stor-spec-list-formalp
- Check if a list of storage class specifiers
has formal dynamic semantics.
- Declor-fun-formalp
- Check if a declarator has formal dynamic semantics,
as part of a function declaration.
- Declor-block-formalp
- Check if a declarator has formal dynamic semantics,
as part of a block item declaration.
- Strunispec-formalp
- Check if a structure declaration has formal dynamic semantics.
- Structdecl-list-formalp
- Check if all the structure declarations in a list
have formal dynamic semantics.
- Param-declon-list-formalp
- Check if all the parameter declarations in a list
have formal dynamic semantics.
- Desiniter-list-formalp
- Check if all the initializers with optional designations in a list
have formal dynamic semantics.
- Extdecl-list-formalp
- Check if all the external declarations in a list
have formal dynamic semantics.
- Expr-list-pure-formalp
- Check if all the expressions in a list have formal dynamic semantics,
as pure expressions.
- Transunit-formalp
- Check if a translation unit has formal dynamic semantics.
- Const-formalp
- Check if a constant has formal dynamic semantics.
- Stmt-formalp
- Check if a statement has formal dynamic semantics.
- Block-item-list-formalp
- Check if a list of block items have formal dynamic semantics.
- Block-item-formalp
- Check if a block item has formal dynamic semantics.
