Logic pour la vérification du logiciel

Question

je regarde les exigences de vérification du logiciel automatisé, soit un programme qui prend en code (code de procédure ordinaire écrite dans des langues comme C et Java), génère un tas de théorèmes en disant que chaque boucle doit éventuellement stop, aucune assertion ne sera violée, il n'y aura jamais de déréférencement d'un pointeur nul etc., puis il passera à un prouveur de théorème pour prouver qu'il est réellement vrai (ou alors trouver un contre-exemple indiquant un bug dans le code).

La question est quel genre de logique à utiliser. Les deux positions principales semblent être:

1. La logique du premier ordre est très bien.

2. logique du premier ordre ne suffit pas d'expression, vous avez besoin d'une logique d'ordre supérieur.

Le problème est qu'il semble y avoir beaucoup de support pour les deux positions. Alors, lequel a raison? Si c'est le second, y a-t-il des exemples de choses que vous voulez faire, que les vérificateurs basés sur la logique du premier ordre ont des problèmes?

Answer 1

Vous pouvez faire tout ce dont vous avez besoin FOL, mais il y a beaucoup de travail supplémentaire - beaucoup! La plupart des systèmes existants ont été développés par des universitaires/des personnes avec peu de temps, ils sont donc tentés de prendre des raccourcis pour gagner du temps/effort, et sont donc attirés par les HOL, les langages fonctionnels, etc. Ce système qui doit être utilisé par des centaines de milliers de personnes plutôt que simplement par des centaines, nous croyons que FOL est la voie à suivre parce qu'elle est beaucoup plus accessible à un plus large public. Il n'y a pas de substitut à faire le travail; Nous y sommes depuis 25 ans maintenant! S'il vous plaît jeter un oeil à notre projet (http://www.manmademinions.com)

Cordialement, Aaron.

Answer 2

Dans mon expérience pratique, il semble être « 1. La logique du premier ordre est très bien ». Pour des exemples de spécifications complètes pour diverses fonctions écrites entièrement dans un langage de spécification basé sur la logique du premier ordre, voir par exemple ACSL by Example ou this case study.

La logique du premier ordre comporte des prouveurs automatisés (pas des assistants de preuve) qui ont été affinés au fil des ans pour gérer les propriétés de puits provenant de la vérification du programme. Les prouveurs automatiques notables pour ces utilisations sont par exemple Simplify, Z3 et Alt-ergo. Si ces prouveurs échouent et qu'il n'y a pas de lemme/assertion évidente que vous pouvez ajouter pour les aider, vous avez encore le recours au démarrage d'un assistant de preuve pour les obligations de preuve difficiles. Si vous utilisez HOL d'un autre côté, vous ne pouvez pas utiliser Simplify, Z3 ou Alt-ergo, et même si j'ai entendu parler des prouveurs automatiques pour la logique d'ordre élevé, je ne les ai jamais vantés pour leur efficacité en matière de propriétés des programmes.

Answer 3

Nous avons constaté que FOL est correct pour la plupart des conditions de vérification, mais une logique d'ordre supérieur est inestimable pour un petit nombre, par exemple pour prouver les propriétés de sommation des éléments dans une collection. Donc, notre prouveur de théorèmes (utilisé dans Perfect Developer et Escher C Verifier) ​​est fondamentalement de premier ordre, mais avec la possibilité de faire un certain raisonnement d'ordre supérieur.