Operating system support for contracts

US9286039B2 · kind B2 · utility

Assignee

• MICROSOFT TECHNOLOGY LICENSING, LLC · US

Inventors

• John Duffy · Renton, US
• Jared Porter Parsons · Kirkland, US
• Colin Gordon · Katy, US
• Alexander Daniel Bromfield · Seattle, US
• Martin Taillefer · Redmond, US
• David Bartolomeo · Lake Stevens, US
• Michael Barnett · Seattle, US

Key dates

• Filing date: Mar 14, 2013
• Grant date: Mar 15, 2016
• Expiry date: May 18, 2033

Classification

• Technology area (CPC G): Physics
• CPC primary: G06F9/54
• WIPO field: Computer technology
• WIPO sector: Electrical engineering

Abstract

A front-end compiler compiles source code into intermediate code, that may later be compiled into binary code. The source code defines an execution scope and includes a contract. When a contract is encountered at runtime of an execution scope, further execution of that execution scope is conditioned on whether a predicate associated with the contract is true. The front-end compiler operates so as to preserve the contract so that the contract continues to be semantically structured such that the predicate may be removed from the intermediate language code. The contract may thus continue to be understood by semantic analysis of the contract. Thus, the predicate may be understood by static analysis tools that operate on the intermediate code.