I den här artikeln visar vi hur vår programtransformationsalgoritm som kallas destillation inte bara kan användas för optimering av program, utan också för att underlätta programverifiering. Med hjälp av destillationsalgoritmen omvandlas program till en specialiserad form där funktionerna är rekursiva i svansen och mycket få mellanliggande strukturer skapas. Vi visar sedan hur egenskaper hos denna specialiserade form av program enkelt kan verifieras genom tillämpning av induktiva bevis regler. Vi hävdar därför att destillationsalgoritmen är en idealisk kandidat för att inkluderas i kompilatorer eftersom det underlättar de två målen för programoptimering och verifiering.
I REF G. W. Hamilton beskrivs med hjälp av sin destillationsalgoritm som en bevisassistent för omvandling av program till en svans rekursiv form i vilken vissa egenskaper hos programmen lätt kan verifieras genom tillämpning av induktiva bevis regler.
Distilling Programs for Verification
{'venue': 'Electron. Notes Theor. Comput. Sci.', 'journal': 'Electron. Notes Theor. Comput. Sci.', 'mag_field_of_study': ['Computer Science']}