4 ms·

> If you want proof of correctness, formal methods are the only game in town. How does this take into account unknown parameters indicated in the parent? For

> If you want proof of correctness, formal methods are the only game in town. How does this take into account unknown parameters indicated in the parent? For instance, expecting little endian but getting big endian in a different environment?

MaxBarraclough 6y ago
With the disclaimer that I'm not an expert on formal methods, or on endianness: endianness is something that could be formally modelled, but it seems to me the better approach is to write code that's insensitive to platform endianness. Another approach might be to ensure such platform-specific assumptions hold true by using static assertions, so that the build will fail if the assumptions are not met. A third approach might be to write (and verify) separate code for different endiannesses. Any one of these approaches should make it possible to write formally verifiable C code that behaves identically regardless of endianness. Of course, by using a formal verification framework, you aren't worrying about being blindsided by something like endianness, you're worrying about getting the thing to verify. If it verifies, that means you haven't made any fiddly mistakes with concerns like endianness. The SPARK language (designed for formal verification) doesn't let you write endian-sensitive code in the first place, if I understand correctly. (SPARK is technically not a fully deterministic language but it's very close. [0][1]) I don't know if there are circumstances where you must write endian-sensitive code, but don't think there are. I can imagine an endian-sensitive solution might perform better (e.g. simply reinterpreting an array of bytes as an array of 32-bit unsigned integers). [0] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#parenthesized-arithmetic-operations https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#benefits-of-using-spark-for-portability https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...

MaxBarraclough 6y ago

With the disclaimer that I'm not an expert on formal methods, or on endianness: endianness is something that could be formally modelled, but it seems to me the better approach is to write code that's insensitive to platform endianness. Another approach might be to ensure such platform-specific assumptions hold true by using static assertions, so that the build will fail if the assumptions are not met. A third approach might be to write (and verify) separate code for different endiannesses. Any one of these approaches should make it possible to write formally verifiable C code that behaves identically regardless of endianness. Of course, by using a formal verification framework, you aren't worrying about being blindsided by something like endianness, you're worrying about getting the thing to verify. If it verifies, that means you haven't made any fiddly mistakes with concerns like endianness. The SPARK language (designed for formal verification) doesn't let you write endian-sensitive code in the first place, if I understand correctly. (SPARK is technically not a fully deterministic language but it's very close. [0][1]) I don't know if there are circumstances where you must write endian-sensitive code, but don't think there are. I can imagine an endian-sensitive solution might perform better (e.g. simply reinterpreting an array of bytes as an array of 32-bit unsigned integers). [0] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#parenthesized-arithmetic-operations https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#benefits-of-using-spark-for-portability https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...