Modèle d'exécution formel pour Java (ou langue impérative générale)

Question

J'essaie de prouver certaines déclarations sur l'exécution dans les programmes Java sous certaines restrictions lourdes (en gros, j'ai une conjecture que si deux méthodes satisfont un ensemble de contraintes pour une entrée donnée, alors sont-ils équivalents - c'est-à-dire que la valeur de retour et l'état après après L'exécution est identique). Pour prouver cela, je recherche une sorte de formalisme qui me permettra de parler de cela.

Je connais la sémantique opérationnelle des langues fonctionnelles et je pourrais éventuellement traduire pour des boucles / tandis que des boucles aux fonctions récursives ... je préfère ne pas le faire et ce serait bien d'avoir des machines afin que je puisse rester dans un pays impératif .

Plus précisément, je veux raisonner sur le Etat d'une méthode au kL'étape d'exécution. Cela inclut l'état mondial:

• Appels comme this.field = 2 Mettez à jour notre état de classe
• Appels Modification des paramètres Mettre à jour l'état en dehors de notre méthode:
  • myParam.setFoo(...)
  • myParam.x = y
• Appels à des méthodes statiques
  • Blah.static_side_effects()

Je suppose que tout cela est déterministe. C'est-à-dire que je veux formaliser l'hypothèse que si l'une de ces mises à jour globales de l'état se produit dans deux méthodes, dont les états d'exécution globaux et locaux sont identiques, alors le nouvel état sera également identique - que chaque étape de calcul est déterminée précisément par l'État mondial et l'État local. Cela empêche évidemment les RNG et le parallélisme (mais je peux y faire face plus tard ...).

Des idées ou des sources sur la façon dont je pourrais aborder cela? Ma seule pensée est de traiter les méthodes comme une liste d'instructions et d'essayer de décrire officiellement une sémantique de déclarations.

Si possible, j'aimerais le faire au niveau de la langue Java plutôt que le niveau JVM. Cela n'est peut-être pas possible, mais mon objectif pour l'instant est de faire des hypothèses raisonnables sur ma sémantique opérationnelle, puis de le prendre à partir de là.

Oh, une dernière note - toute suggestion sur la façon dont je peux améliorer cette question serait grandement appréciée. Je suis en quelque sorte en train d'essayer de trouver la bonne langue pour poser la question et si j'abuse de la terminologie (comme l'état d'exécution local / mondial ...) j'adorerais corriger cela.