FCL: A FORMAL LANGUAGE FOR WRITING CONTRACTS

Abstract

Contracts are legally enforceable agreements between two or more parties. The agreements can contain temporally based conditions, such as actions taken by the contract parties or events that happen, that trigger changes to the state of the contract when the conditions become true. Since the structure of these conditions can be very complex, it can be difficult to write contracts in a natural language in a clear and unambiguous way. A better approach is to have a formal language with a precise semantics to represent contracts. Contracts expressed in such a language have a mathematically precise meaning and can be written, analyzed, and manipulated by software. This thesis presents FCL, a formal language with a precise semantics for writing general contracts that may depend on temporally based conditions. Motivated by carefully selected examples of contracts, we derive a set of desirable requirements that a formal language of contracts should support. Based on the requirements, we clearly de ne the notion of contract and address what it means to fulfill or breach a contract. We present the formal syntax and semantics of FCL. We also successfully formalize different kinds of contracts in FCL and develop a reasoning system for FCL.