User loginNavigation |
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