4 ms·
Talking about statically-typed languages and configuration paramètres, something coming from the Ada/SparkAda world is the use of type predicates and invariants
by touisteur 9y ago
Talking about statically-typed languages and configuration paramètres, something coming from the Ada/SparkAda world is the use of type predicates and invariants, in addition to expressive static typing.
Here's an interesting paper on the subject : http://acg-solutions.fr/acg/wp-content/uploads/2017/04/PDI-5.pdf http://acg-solutions.fr/acg/wp-content/uploads/2017/04/PDI-5...
And here's some demo code : https://github.com/AdaCore/SPARK_PDI_Demo/blob/master/README.md https://github.com/AdaCore/SPARK_PDI_Demo/blob/master/README...
The other interesting part is that you can then prove (or use static analysis to get à high level of confidence) your application will never be run with incoherent parameters. Another nice thing is that with the help of the prover you can let the internal constraints of your implementation surface up to the application parameters. Sa y you didn't handle some corner case, you can either implement it, or use a predicate to ensure this case is never run. Your pre-conditions and the type invariants/predicates of your parameters are part of your interface.