Logic Programming Tools for Formal Software Specification

Abstract

Jednym z najistotniejszych problemów w inżynierii oprogramowania jest opracowanie i zawężenie wymagań dotyczących oprogramowania w celu określenia dokładnych specyfikacji, a także kwestia przekształcenia specyfikacji dotyczących złożonych problemów w wykonywalne kody. Głównym powodem podjęcia się badania formalnych specyfikacji jest udowodnienie, że oprogramowanie produkowane jest z nimi zgodne (chodzi o weryfikowalność). Artykuł ukazuje, iż programowanie logiczne połączone z rachunkiem sytuacyjnym można z powodzeniem stosować jako formalną specyfikację oprogramowania.