Detta dokument beskriver en ny teknik för syntes av tvingande program. Automatiserad programsyntes har potential att göra programmering och utformning av system enklare genom att tillåta program att specificeras på en högre nivå än körbar kod. I vårt tillvägagångssätt, som vi kallar proof-theoretic syntes, ger användaren en input-output funktionell specifikation, en beskrivning av atomverksamheten i programmeringsspråket, och en specifikation av det syntetiserade programmets looping struktur, tillåten stack utrymme, och bunden på användning av vissa operationer. Vår teknik syntetiserar ett program, om det finns ett, som uppfyller inputoutput specifikationen och använder bara de givna resurserna. Insikten bakom vårt tillvägagångssätt är att tolka programsyntesen som generell programverifiering, vilket gör att vi kan föra verifikationsverktyg och tekniker till programsyntes. Vår syntesalgoritm fungerar genom att skapa ett program med okända uttalanden, vakter, induktiva invarianter och rankingfunktioner. Det genererar sedan begränsningar som relaterar de okända och tillämpar tre typer av krav: partiell korrekthet, loop terminering, och väl formade villkor på programvakter. Vi formaliserar de krav som programverifieringsverktyg måste uppfylla för att lösa dessa begränsningar och använda verktyg från tidigare arbete som våra syntar. Vi visar genomförbarheten av det föreslagna tillvägagångssättet genom att syntetisera program inom tre olika områden: aritmetisk, sortering och dynamisk programmering. Med hjälp av verifieringsverktyg som vi tidigare byggt i VS 3-projektet kan vi syntetisera program för komplicerade aritmetiska algoritmer inklusive Strassens matrismultiplikation och Bresenhams linjeritning; flera sorteringsalgoritmer; och flera dynamiska programmeringsalgoritmer. För dessa program, är mediantiden för syntes 14 sekunder, och förhållandet mellan syntes till verifieringstid varierar mellan 1× till 92× (med en median på 7×), som illustrerar potentialen i metoden.
Srivastava m.fl. REF beskrev en ny teknik för programvaruverifiering genom att införa syntesen av tvingande program.
From program verification to program synthesis
{'venue': "POPL '10", 'journal': None, 'mag_field_of_study': ['Computer Science']}