W niniejszej pracy przeanalizowane zostały przykłady zapisu projektów implementacji nieograniczonego stosu liczb całkowitych w środowisku systemu automatyzacji weryfikacji PVS. Po sformułowaniu paru przykładów opierających się na standardowych typach danych okazało się, iż prostszym i bardziej eleganckim przedstawieniem różnych rodzajów projektów implementacji (zdecentralizowanych, scentralizowanych i mieszanych) jest stworzenie projektów wielomodułowych wykorzystujących (w tym przypadku) projekt interfejsu modułu ograniczonej kolekcji do przechowywania obiektów implementowanego typu. W tym celu powstał projekt interfejsu i (dopełniający go) projekt implementacji modułu . Aby ułatwić dowody poprawności projektu interfejsu zmieniono reprezentację tropów w PVS, z odwróconych list (jak np. w [3]) na skończone sekwencje. Konsekwentnie wszystkie prezentowane w tej pracy przykłady wykorzystują tę nową reprezentację tropów.

Efektem analizy i spostrzeżeń poczynionych podczas prac nad formułowaniem przykładów wielomodułowych jest modyfikacja dotychczasowej klasyfikacji projektów implementacji. Proponuje się możliwość chwilowej rezygnacji z zasady czarnej-skrzynki i dopuszcza tzw. otwarte projekty implementacji pojedynczego obiektu wykorzystujące do opisania obiektów implementowanego typu inne projekty implementacji. Wprowadza się pojęcie obszaru zależności otwartego projektu implementacji, który razem z tym projektem stanowi domknięty projekt implementacji, spełniający już (względem innych modułów) zasadę ukrywania sposobu realizacji struktury wewnętrznej.

Kolejną proponowaną zmianą jest zarzucenie podziału na zdecentralizowane, scentralizowane i mieszane projekty implementacji i formułowanie jedynie projektów implementacji ADT. Dotychczasowy podział ze względu na miejsce przechowywania obiektów (u klienta, w module, zarówno u klienta, jak w module) przeniesiony został na schematy tworzenia wielomodułowych projektów implementacji. W ten sposób koncentrując się na opisie konkretnego typu danych abstrahuje się od różnych koncepcji przechowywania obiektów. Dopiero następną fazą jest zastosowanie odpowiedniego schematu do projektu (lub projektów) implementacji pojedynczego obiektu i uzykanie w ten sposób pożądanego sposobu implementacji i przechowywania obiektów w ramach modułu.