> Сначала правильность алгоритма докажите.
> А дальше - пойдут нежданчики со стороны форматов представления данных, их выравнивания, округлений, точностей...Вообще-то, любой мал-мальско серьезный "formal verification" различает между понятиями "логика" и "реализация". И в нормальное доказательство соотв. конкретной реализации алгоритму, вот это все вышеупомянутое вполне входит.
Классика:
https://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4...
> Formal Verification of an OS Kernel
> The most detailed layer in our verification is the C implementation. The translation from C into Isabelle is correctness-critical and we take great care to model the semantics of our C subset precisely and foundationally. Precisely means that we treat C semantics, types, and memory model
...
> As kernel programmers do, we make assumptions about the compiler (GCC) that go beyond the standard, and about the architecture used (ARMv6). These are explicit in the model, and we can therefore detect violations. Foundationally means that we do not just axiomatise the behaviour of C on a high level, but we derive it from first principles as far as possible. For example, in our model of C, memory is a primitive function from addresses to bytes without type information or restrictions. On top of that, we specify how types like unsigned int are encoded, how structures are laid out, and how implicit and explicit type casts behave. We managed to lift this low-level memory model to a high-level calculus that allows efficient,
...
> 4.4 Machine model
> Programming in C is not sufficient for implementing a kernel. There are places where the programmer has to go outside the semantics of C to manipulate hardware directly. In the easiest case, this is achieved
Недостаток (помимо требования нехилой такой квалификации):
> seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler.
...
> The cost of the proof is higher, in total about 20 py.
.
