Jednym z podejść do systematycznego tworzenia oprogramowania jest tzw. podejście funkcyjne [9]. Zgodnie z jego zaleceniami, przy projektowaniu systemów komputerowych powinien powstać odpowiedni zestaw dokumentów, zawierających wszystkie informacje niezbędne do walidacji specyfikacji wymagań oraz do weryfikacji kolejnych etapów procesu opracowywania końcowego produktu. Obejmuje on specyfikację wymagań, projekt systemu i przewodnik po modułach, a następnie dla każdego modułu: projekt interfejsu oraz projekt implementacji. Przez moduł rozumie się tutaj moduł programu, czyli funkcjonalnie odrębną część większego oprogramowania, który jest równocześnie modułem programistycznym, stanowiącym zadanie zlecane programiście do realizacji*. Preferowaną w podejściu funkcyjnym metodą specyfikacji interfejsu modułu jest Metoda Tropów (ang. Trace Assertion Method, w skrócie TAM) [4]. Formalizuje ona zadanie tworzenia projektu interfejsu, który zgodnie z zasadą "czarnej skrzynki" abstrahuje od szczegółów wewnętrznych opisując jedynie sposób interakcji modułu z otoczeniem. Na tym poziomie opisuje się abstrakcyjny typ danych, którego modyfikacje są możliwe poprzez odpowiednio przygotowane programy, zwane programami dostępu. Kolejnym etapem podejścia funkcyjnego jest projekt implementacji określający wewnętrzną strukturę modułu i sposób realizacji jego funkcji. Wyznacza się konkretny typ danych służący do implementacji specyfikowanego typu oraz dla każdego programu dostępu tworzy się odpowiednią tzw. LD-relację [10], która opisuje efekt wywołania tego programu. Do wykazania semantycznej poprawności projektu implementacji oraz jego zgodności z projektem interfejsu tworzy się zbiór obligacji pod postacią formuł logicznych. Dzięki wyrażeniu obligacji w języku logiki jest możliwe ich dowodzenie przy użyciu systemu automatyzacji weryfikacji.

Celem niniejszej pracy jest zbadanie na przykładach wypracowanego wcześniej sposobu tłumaczenia ([1]) projektów implementacji na język formalnej specyfikacji systemu PVS (ang. Prototype Verification System [7], [8]), który jest jednym z owych systemów wspomagających weryfikację. Skrótowy opis kolejnych etapów dokumentacji modułu można znaleźć w rozdziale 2. Podstawowe zasady zanurzenia projektów interfejsu i implementacji oraz sposób formułowania obligacji w języku specyfikacji PVS przedstawiono w rozdziale 3. W rozdziale 4 są rozpatrywane przykłady konstrukcji różnych typów projektów implementacji. Większość przykładów, to projekty implementacji nieograniczonego stosu liczb całkowitych będących ukonkretnieniem projektu interfejsu opisanego m. in. w [6].