Abstrakt. Fyra bevisregler för rekursiva förfaranden på ett Pascal-liknande språk presenteras. Huvudregeln handlar om total korrekthet och är baserad på resultat från Gries och Martin. Regeln är lättare att tillämpa än Martins. Det införs som en utvidgning av ett specifikationsformat för Pascal-förfaranden, med tillhörande regler om korrekthet och inkallelse. Det använder välgrundade rekursion och bevisas under postulatet att ett förfarande är semantiskt lika med sin kropp. Denna regel om total korrekthet jämförs med Hoares regel om partiell korrekthet i rekursiva förfaranden, där inget välgrundat samband behövs. Båda reglerna är korrekta, d.v.s. vissa förutsättningar är tillräckliga. Det finns också två regler för att visa att förutsättningar är nödvändiga. Dessa regler kan användas för att ge formella bevis på icke-avslutande och förfining. De verkar vara helt nya.
Hesselink REF gav flera bevisregler för rekursiva förfaranden, både för fullständig och partiell korrekthet.
Proof rules for recursive procedures
{'venue': 'Formal Aspects of Computing', 'journal': 'Formal Aspects of Computing', 'mag_field_of_study': ['Computer Science']}