SHF: Small: Effectful Software Contracts

点击翻译按钮获取中文摘要

The long-term goals of this project are to bring the technology of software contracts to widely-used programming languages and, throughthe use of manifest contracts, to provide software developers with a migration path from simply-typed code to fully functional correctness. Since computational effects are notoriously hard to reason about andpervade even the simplest realistic programs, the proposed research should have significant impact on programmers' ability to developsoftware that is more reliable and more secure. Contracts in software establish clear interfaces between program components. Like contracts in the legal realm, they delineate eachparty's expectations and obligations. Such contracts are becoming increasingly important for the regulation of modern software systems,providing an expressive framework for verification and error tracking. To be effective in a software environment, contracts must have formal semantics and must be supported by a monitoring system that preciselytracks the flow of values as they cross interfaces. To date, however, the formal study of contracts has mostly been limited to smallidealized languages without computational effects, such as reading data from or writing data to a display or file, managing resourcessuch as memory, and performing probabilistic or speculative computation.This research aims to extend the semantic framework of software contracts to languages with various computational effects: theextension is qualitative in nature and will enable the use of contracts in new application domains. Specifically, the PIs proposeto add support for computational effects to the two flavors of contracts studied to date: latent contracts, which are runtime checksnot reflected in the type system, and manifest contracts, where a system of precise types records the most recent runtime check appliedto each value. The extension of latent contracts will be done in the context of a monadic meta language. The extension of manifestcontracts will make use of a variant of Hoare Type Theory to precisely record computational effects. The PIs will also implement prototype systems and use them to present novel applications of softwarecontracts.