Changes between Initial Version and Version 1 of Commentary/Contracts


Ignore:
Timestamp:
Jun 20, 2011 2:01:16 PM (3 years ago)
Author:
cpa
Comment:

Very first version!

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Contracts

    v1 v1  
     1= Contracts for Haskell = 
     2 
     3== Involved == 
     4 * Simon Peyton-Jones 
     5 * Dimitrios Vytiniotis 
     6 * Koen Claessen 
     7 * Charles-Pierre Astolfi 
     8 
     9 
     10== Overview == 
     11 
     12Contracts, just as types, give a specification of the arguments and return values of a function. For example we can give to head the following contract: 
     13 
     14{{{ 
     15head ::: {x | not (null x)} -> Ok 
     16}}} 
     17 
     18Where Ok means that the result of head is not an error/exception as long as the argument isn't. 
     19 
     20 
     21Any Haskell boolean expression can be used in a contract, for example 
     22{{{ 
     23fac ::: a:Ok -> {x | x >= a} 
     24}}} 
     25is a contract that means that for every a which is an actual integer (not an error), then fac a >= a 
     26 
     27 
     28We can also use a higher-order contracts: 
     29{{{ 
     30map ::: ({x | x >= 0} -> {x | x > 0}) -> {xs | not (null xs)} -> Ok 
     31}}} 
     32This contract means that if we apply map to a non-empty list with a function that takes a non-negative integer and returns an positive integer then map returns a list of values without errors. 
     33 
     34 
     35For a formal introduction, one can read [1]. 
     36 
     37== The plan == 
     38Verifying that a function satisfies a given contract is obviously undecidable, but that does not mean that we can't prove anything interesting. Our plan is to translate Haskell programs to first-order logic (with equality) and then use Koen's automated theorem prover to check contract satisfaction. Given that first-order logic is only semi-decidable, the theorem prover can (and in fact does) hang when fed with contracts that are in contradiction with the function definition. 
     39 
     40== Current status == 
     41The current status is described in [3] and some code and examples can be found in [2]. Note that given it's just a prototype the input syntax is slightly different from Haskell. In the end, we should get a ghc extension for contracts. 
     42 
     43== Questions == 
     44 * Do we need cfness predicate anymore? It was important in the POPL paper but is still relevant? 
     45 * UNR should be renamed to a less confusing name. 
     46 * Hoare logic vs liquid types 
     47 * Semantics & domain theory to prove the correctness of the translation 
     48 * Unfolding for proving contracts on recursive functions 
     49 
     50 
     51== References == 
     52[1] : http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm [[BR]] 
     53[2] : https://github.com/cpa/haskellcontracts and https://github.com/cpa/haskellcontracts-examples [[BR]] 
     54[3] : https://github.com/cpa/haskellcontracts/blob/master/draft2.pdf