An abstract state machine models a C program as states that change through execution. Its states include observable variable contents and output, while transitions are governed by values, types, and binary representations rather than a particular hardware implementation. section 5.1 section 5.1.3
Following a value through execution
double x = 5.0; double y = 3.0; x = (x * 1.5) - y; printf("x is %g\n", x); The abstract execution can be read as x, then (5.0 * 1.5), then 7.5 - 3.0, then x = 4.5, followed by output of 4.5. section 5.1
Programs execute as if they followed this model. A compiler may remove unused assignments, replace several operations with one, or reorder independent work when the observable result remains unchanged. It must preserve effects such as output and consequences that depend on the value's type, including possible overflow or termination. section 5.1.3 section 5.1.4
Key consequences:
- Reason primarily about values instead of assuming a particular machine representation. section 5.0
- Treat type as a constraint on valid transformations and optimization opportunities. section 5.1.4
double x = 5.0;
double y = 3.0;
...
x = (x * 1.5) - y;
printf("x is \%g\n", x);
!@%STYLE%@!
{"css":"{\"css\": \"font-weight: bold;\"}","target":"[[{\"line\":0,\"ch\":3},{\"line\":0,\"ch\":9}],[{\"line\":1,\"ch\":3},{\"line\":1,\"ch\":9}],[{\"line\":0,\"ch\":3},{\"line\":0,\"ch\":9}],[{\"line\":1,\"ch\":3},{\"line\":1,\"ch\":9}],[{\"line\":4,\"ch\":3},{\"line\":4,\"ch\":9}]]"}
!@%STYLE%@!
Trace the complete example from variable initialization through arithmetic assignments to the printed result. section 5.1
