Hur vet vi att ett datorprogram gör vad det säger att det gör? Formell verifiering av hypergeometriska rekursionsrelationer med polynomkoefficienter

Abstract

Detta arbete använder formell verifiering för att undersöka loopar inom programmering. Looparna som behandlas ses ekvivalent som hypergeometriska rekursionsrelationer. Arbetet undersöker om lösningen un till dessa hypergeometriska rekursionsrelationer med polynomkoefficienter alltid är heltalsvärd. Detta genomförs under antagandet att startvärdet för rekursionsrelationen alltid är 1. För koefficienter som är vissa typer av linjära polynom ges villkor som avgör om un alltid är ett heltal. Även mer involverade typer av polynom undersöks, där en explicit algoritm ges som avgör om un alltid är ett heltal efter ändligt antal steg. Resultaten för det sistnämnda fallet generaliseras även till flera variabler.