返回Google圖書搜尋

Should Your Specification Language be Typed?

出版	Digital, Systems Research Center, 1997
URL	http://books.google.com.hk/books?id=scUgAQAAIAAJ&hl=&source=gbs_api

註釋Abstract: "Most specification languages have a type system. The languages used in some popular textbooks have half-baked type systems that are described informally and never spelled out in detail. Such type systems tend to have unexpected consequences, if not outright inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Set theory is simpler and more flexible than most typed formalisms. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased complexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verification, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages."