We propose a small extension of the ERLANG language that allows programmers to specify contracts with type information at the level of individual functions. Such contracts are optional and they document the intended uses of functions. Contracts allow automatic documentation tools such as Edoc to generate better documentation and defect detection tools such as Dialyzer to detect more type clashes. Since the Erlang/OTP system already contains components which perform automatic type inference of success typings, we also describe how contracts interact with success typings and can often provide some key information to the inference process. Categories and Subject Descriptors F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--Type structure; D.2.7 [Software Engineering]: Distribution, Maintenance, and Enhancement--Documentation General Terms Design, Documentation, Languages, Verification Keywords Erlang, success typings, contracts
Miguel Jimenez, Tobias Lindahl, Konstantinos F. Sa