>Horst,
>
>One thing about what you say confuses me a bit. If a "complete and
>sound formal semantic[s] for C" is so difficult, what are compiler
>writers using when they write code generators for C (or any other
>procedural programming language)? It seems that if there is something
>missing or unintentionally ambiguous in the existing specifications
>(regardless of how formal you consider them) of the language, then it
>would not be possible to write reliable or predictable programs at
>all.
The real challenge extends beyond proving C programs correct. Linux
has many environments which have implicit preconditions. Cases where
the code should never go into a wait. What with the preprocessor,
interrupts,locking, inline functions, and a() calling b() calling c()
calling d(), verifying the implicit preconditions is tough. That is
what a Linux-lint should be targetted at, IMHO.
john alvord
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/