Developing a Modal Specification Language
Loading...
Authors
Arney, David
Issue Date
2001
Type
Thesis
Language
en_US
Keywords
Alternative Title
Abstract
Meta-logical frameworks are used to create and analyze formal specifications of programming languages. This research builds upon McDowell and Miller's meta-logical framework FOƛ ∆N. FOƛ ∆N separates the meta-logic used for reasoning from the specification language in which the programming language is encoded. This separation adds a level of indirection that can make the specification cumbersome. The modal meta-logic we designed avoids this indirection by making the specification language a subset of the meta-logic, using a modal operator to distinguish the specification from statements about the specification. We prove that our logic's specification language subset is equivalent to first-order logic, the specification language used in FOƛ ∆N.
Description
iv, 27 p.
Citation
Publisher
License
U.S. copyright laws protect this material. Commercial use or distribution of this material is not permitted without prior written