|
|
|---|
|
|
|
|---|
ATC tutorial: Approach to Generating C Code from ACL2.
ATC translates a subset of ACL2 to C. The ACL2 subset is designed to be close to C, i.e. to be essentially ``C written in ACL2'', so that it is relatively easy to translate to C. There is a direct translation to the C constructs from their representation in ACL2.
ATC is meant to be used in conjunction with APT. One uses APT transformations to refine ACL2 specifications and code to the subset recognized by ATC, which ATC translates to C. Thus, ATC can be used at the end of an APT derivation.
Currently ATC recognizes a limited subset of ACL2 and translates it to a limited subset of C. We plan to extend ATC to increasingly larger subsets of ACL2 and C.
Previous: Comparison with ATJ's Java code generation from ACL2