Ce que tu cherche à faire s'appelle Haskell ou dialyzer pour erlang. ça vérifie les input/output des fonctions et ça permet aussi de le faire en cas d'effets de bord.
Mais comme tu l'as dit, prouver un algorithme est différent de tester une implémentation.
Donc là ton système est supposé faire comme toi, inventer des specs ou il n'y en a pas et avertir le développeur qu'ils s'est probablement trompé ... Un algorithme ce n'est pas des mathématiques, c'est plus que ça, ça témoigne d'une intention. Une machine ne peut pas deviner ce que tu veux faire. Elle peut juste faire ce que tu lui demande de faire parmi un nombre limité d'instructions.
Mais comme tu l'as dit, prouver un algorithme est différent de tester une implémentation.
Code :
function square(int x) {
return 42
}Donc là ton système est supposé faire comme toi, inventer des specs ou il n'y en a pas et avertir le développeur qu'ils s'est probablement trompé ... Un algorithme ce n'est pas des mathématiques, c'est plus que ça, ça témoigne d'une intention. Une machine ne peut pas deviner ce que tu veux faire. Elle peut juste faire ce que tu lui demande de faire parmi un nombre limité d'instructions.