Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Fundamenta Informaticae

1 2000

Powiadomienia systemowe

Sesja wygasła!

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: shallow and deep embedding

Sortuj według:

Ogranicz wyniki do:

Towards automated consistency checking of module interface specifications

Engel M., Kret A., Mincer-Daszkiewicz J.

Fundamenta Informaticae

2000

Vol. 42, nr 3,4

251-278

The Trace Assertion Method (TAM) pioneered by Parnas is a formalism used to specify software module interfaces. The main purpose of the research described in this paper is to recognize the possibilities of linking the TAM editor with one of the existing theorem proving systems and to enable thereby the automated consistency checking of trace specifications. Possible approaches to embedding TAM in the Prototype Verification System (PVS) specification language are discussed and the chosen shallow definitional embedding is described in detail. Proof obligations for the consistency checking of trace specifications are obtained as type correctness conditions generated automatically by the PVS type checker. Some of these obligations can be proven automatically by PVS, other proofs need human guidance. Possible ways of increasing automation capabilities of the PVS theorem prover are recognized and presented. We share our experience in defining both specialized and general purpose proof strategies. This research may be viewed as a case study in applying the existing general purpose proof system to consistency checking of some application-specific formalism, which might be of interest for the software designer community