2 ms·
>His idea with weakest preconditions was to derive code from the desired logical properties, not to prove that a priori written code satisfies those properties,
by mrtesthah 1y ago
>His idea with weakest preconditions was to derive code from the desired logical properties, not to prove that a priori written code satisfies those properties, reckoning that his way would be less work and result in more elegant programs.
I love the idea. Are you aware of any such spec-based code generators in widespread use today?
- csb6 1y agoThe most developed one I know of is Atelier B [0], which uses the B-Method and has a C code generator. I believe this was the tool used to develop several driverless train control systems in the Paris Metro and other subways. There is a free version but unfortunately it is not open source. [0] https://www.atelierb.eu/en/ https://www.atelierb.eu/en/