## User login## Navigation |
## An operational and axiomatic semantics for non-determinism and sequence points in CIn a recent LtU discussion, naasking comments that "I always thought languages that don't specify evaluation order should classify possibly effectful expressions that assume an evaluation order to be errors". Recent work on the C language has provided reasonable formal tools to reason about evaluation order for C, which has very complex evaluation-order rules. An operational and axiomatic semantics for non-determinism and sequence points in C
One aspect of this work that I find particularly interesting is that it provides a program (separation) logic: there is a set of inference rules for a judgment of the form \(\Delta; J; R \vdash \{P\} s \{Q\}\), where \(s\) is a C statement and \(P, Q\) are logical pre,post-conditions such that if it holds, then the statement \(s\) has no undefined behavior related to expression evaluation order. This opens the door to practical verification that existing C program are safe in a very strong way (this is all validated in the Coq theorem prover). |
## Browse archives## Active forum topics |

## Recent comments

1 hour 6 min ago

2 hours 34 min ago

4 hours 8 min ago

5 hours 48 min ago

15 hours 46 min ago

15 hours 51 min ago

19 hours 54 min ago

20 hours 15 min ago

20 hours 50 min ago

21 hours 11 min ago