## 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

12 weeks 3 days ago

12 weeks 3 days ago

12 weeks 3 days ago

34 weeks 4 days ago

38 weeks 6 days ago

40 weeks 4 days ago

40 weeks 4 days ago

43 weeks 1 day ago

47 weeks 6 days ago

47 weeks 6 days ago