PlusCal

Valider formellement un algorithme permet, de s’assurer que le design ne contient pas de faute de logique. Pour de petits algorithmes, il est plutôt simple d’avoir en tête la liste de tous les états possibles du systèmes. Mais lorsque l’on prend en compte de la concurrence ainsi que du non-déterminisme rajouté par le réseau, ce n’est pas possible d’avoir en tête l’entièreté des états possibles du système. La Vérification Formelle est le fait de prouver l’exactitude d’un système par rapport à une spécification formelle et des propriétés, utilisant des méthodes formelles mathématiques. Il existe différents types de vérification formelle, certaines permettent de vérifier des algorithmes, d’autres des implémentations. ...

Formally validating an algorithm ensures that the design does not contain any logical errors. For small algorithms, it is fairly simple to keep track of all possible states of the system. However, when concurrency and non-determinism added by the network are taken into account, it is not possible to keep track of all possible states of the system. Formal verification is the process of proving the correctness of a system against a formal specification and properties, using formal mathematical methods. There are different types of formal verification, some of which can be used to verify algorithms, others to verify implementations. ...