Esiste una connessione formale / accademica tra un programma imperativo e l'algebra e, in caso affermativo, dove dovrei imparare a riguardo?
L'esempio che sto pensando è:
if(C1) { A1(); A2(); }
if(C2) { A1(); A2(); }
Rappresentato come una somma di termini:
(C1)(A1) + (C1)(A2) + (C2)(A1) + (C2)(A2) = (C1+C2)(A1+A2)
L'idea è che la manipolazione potrebbe portare a un refactoring programmatico - il "factoring" è il concetto comune in questo esempio.
Come altri hanno sottolineato, c'è molta ricerca esistente sui metodi formali per l'analisi del programma. Un mio ex collega è un ricercatore attivo in questo settore e sua pagina fornisce diversi indicatori su dove iniziare.
Ci sono diverse parole chiave in quell'area, ognuna delle quali genera in genere un'intera area di ricerca stessa. Quindi, la tua domanda non può essere pienamente risolta qui, ma possiamo almeno fornire qualche direzione. Per la maggior parte, questi approcci sono separati in tre rami:
E proprio come in fisica, siamo anche interessati a unificare questi rami, a quel punto si entra nel regno delle teorie unificate della programmazione .
Ci scusiamo per non aver dato una risposta specifica alla domanda, ma c'è tutto il materiale disponibile per tenerti occupato per alcuni decenni e, a meno che non sia in mente un'applicazione desiderata, non è davvero possibile fare una scelta da questi .
Leggi altre domande sui tag refactoring static-analysis formal-methods