Contracts

Design by Contract for Elixir

Usage

useContractsrequiresx>0ensures(result*result)<=x&&(result+1)*(result+1)>xdefsqrt(x)do:math.sqrt(x)end

Bigger example

defmoduleTankdodefstructlevel: 0,max_level: 10,in_valve: :closed,out_valve: :closeduseContractsrequiresnotfull?(tank)&&tank.in_valve==:open&&tank.out_valve==:closedensuresfull?(result)&&result.in_valve==:closed&&result.out_valve==:closeddeffill(tank)do%Tank{tank|level: 10,in_valve: :closed}endrequirestank.in_valve==:closed&&tank.out_valve==:openensuresempty?(result)&&result.in_valve==:closed&&result.out_valve==:closeddefempty(tank)do%Tank{tank|level: 1,out_valve: :closed}# %Tank{tank | level: 0, out_valve: :closed} # correct implementationenddeffull?(tank)dotank.level==tank.max_levelenddefempty?(tank)dotank.level==0endend