This package provides an interface for Design By Contract programming in Julia. The method for software design was first introduced in the Eiffel programming language and has been adapted to other production languages such as Java and C++. It has since been praised by producing readable, easily testable code.
Design By Contract prescribes formal conditions to the execution of a method. One must define the prerequisites and post-conditions expected so that the function is better described and, thus, contributes to the general safety of the program’s state.
This package hasn’t been added to the main Julia repository yet. To use it, one must run:
pkg> add https://github.com/ghaetinger/DesignByContract.jl
DesignByContract.jl works by processing a block containing the prerequisites, post-conditions and the contract’s function.
Prerequisites have the unique goal of filtering the arguments of the function and blocking invalid ones that come from different parts of a program. This can help finding errors in other functionalities as soon as possible. Here is an example of a function that has prerequisites breached:
using DesignByContract
maxDictSize = 2
# Function for adding a variable to a string-key dictionary with a non-null key
@contract begin
require(length(dict) < maxDictSize, length(key) > 0)
function putItem!(dict :: Dict{String, Any}, key :: String, item)
dict[key] = item
return nothing
end
endputItem! (generic function with 1 method)
fruits = Dict{String, Any}()
putItem!(fruits, "apple", :red)
fruitsDict{String,Any} with 1 entry:
"apple" => :red
putItem!(fruits, "blueberry", :blue)
fruitsDict{String,Any} with 2 entries:
"apple" => :red
"blueberry" => :blue
putItem!(fruits, "", :purple)Breach on Requirement Expression 'length(dict) < maxDictSize' in function 'putItem!'
:
Stacktrace: [1] putItem! at ./In[15]:0 [inlined] (repeats 2 times) [2] top-level scope at In[18]:1
delete!(fruits, "blueberry")
putItem!(fruits, "", :purple)Breach on Requirement Expression 'length(key) > 0' in function 'putItem!'
:
Stacktrace: [1] putItem! at ./In[15]:0 [inlined] (repeats 2 times) [2] top-level scope at In[19]:2
Post-conditions work to find errors inside the contracted function. It is also used to find errors easily and as soon as possible. Here is an example of a function that breaches its post-conditions:
minVal = 5
# Function that adds 1 to the values
# of an int array with len > 5
# and guarantees the sum of its elements
# will be > minVal
@contract begin
require(length(arr) >= 5)
ensure(sum(arr) > minVal)
function incrArr!(arr :: Array{Int64, 1})
for index in 1:length(arr)
arr[index] += 1
end
return nothing
end
endincrArr! (generic function with 1 method)
arr = collect(1:5)
display(arr)
incrArr!(arr)
arr5-element Array{Int64,1}:
1
2
3
4
5
5-element Array{Int64,1}:
2
3
4
5
6
arr = collect(ones(Int64, 5))
display(arr)
incrArr!(arr)
arr5-element Array{Int64,1}:
1
1
1
1
1
5-element Array{Int64,1}:
2
2
2
2
2
arr = collect(-1 .* ones(Int64, 5))
display(arr)
incrArr!(arr)
arr5-element Array{Int64,1}:
-1
-1
-1
-1
-1
Breach on Ensure Expression 'sum(arr) > minVal' in function 'incrArr!'
:
Stacktrace:
[1] incrArr!(::Array{Int64,1}) at ./In[24]:15
[2] top-level scope at In[27]:3
It’s important to make sure there are return expressions where you want to
return a value. This is both to make sure you understand the endpoints of the
function and to enable the macro @contract to see them as well. This helps
when you want to ensure the result value. Having this said, we can use the name
result inside ensure expressions to test the returning value. The following
is an example:
# returns the value of a sum or product operation in
# an integer array depending on the parity of it's size.
# Says the final value is positive
@contract begin
ensure(result > 0)
function processArr(arr :: Array{Int64, 1})
if length(arr) % 2 == 0
return prod(arr)
else
return sum(arr)
end
end
endprocessArr (generic function with 1 method)
processArr([1, 2, 3])6
processArr([2, 2, 2, 2])16
processArr([1, 2, 3, -1])Breach on Ensure Expression 'result > 0' in function 'processArr'
:
Stacktrace:
[1] processArr(::Array{Int64,1}) at ./In[5]:8
[2] top-level scope at In[8]:1
Since there could probably be variables in your function with result as name,
there is an extra sub-agreement in the contract block to change the result
name. This sub-agreement is the attribution to the name returnName, e. g.:
# Like the last example but with a twist
@contract begin
returnName = returnValue
ensure(returnValue > 0)
function newProcessArr(arr :: Array{Int64, 1})
result = 0
if length(arr) % 2 == 0
result = prod(arr)
else
result = sum(arr)
end
return -1 * result
end
endnewProcessArr (generic function with 1 method)
newProcessArr([1, 2, 3, -1])6
newProcessArr([2, 2, 2, 2])Breach on Ensure Expression 'returnValue > 0' in function 'newProcessArr'
:
Stacktrace:
[1] newProcessArr(::Array{Int64,1}) at ./In[14]:12
[2] top-level scope at In[16]:1
Loop invariant is a functionality to help writing loops in a way that you don’t
really have to check for exit conditions after every shallow layer
expressions. Take this example:
@macroexpand @loopinvariant (a>0) while(a > 10)
a -= 10; a=2
endquote
if a > 0
nothing
else
throw(ContractBreachException(nothing, "a > 0", "Breach on Loop Invariant Expression"))
end
while a > 10
#= In[3]:2 =#
if a > 0
nothing
else
throw(ContractBreachException(nothing, "a > 0", "Breach on Loop Invariant Expression"))
end
a -= 10
if a > 0
nothing
else
throw(ContractBreachException(nothing, "a > 0", "Breach on Loop Invariant Expression"))
end
#= In[3]:2 =#
if a > 0
nothing
else
throw(ContractBreachException(nothing, "a > 0", "Breach on Loop Invariant Expression"))
end
a = 2
end
end
This way, you’ll check the conditions in every shallow point inside the loop.
When considering your staging code, you should be using the condition check at all times. Some might say that this should also be taken to the deployed code. Andrew Hunt and David Thomas (Pragmatic Programmer, 1999), say that the Design by Contract methodology should be used in running production code, as finding flaws in user runtime is better than not finding flaws at all.
However, the amount of checks can scale with the amount of functions, loops and returns, meaning the efficiency might drop considerably or just a little bit. Since Julia is all about efficiency, we added a function call that disables the expression check filling. There might still be an efficiency decrease in @loopInvariant calls, but it’s constant.
You might want to do this as follows:
julia> @time @loopinvariant (a >= 0) for i = 1:100000000
a += 1
end
6.006486 seconds (100.00 M allocations: 1.490 GiB, 1.30% gc time)
julia> setAgreementEnabling(false)
false
julia> @time @loopinvariant (a >= 0) for i = 1:100000000
a += 1
end
2.812840 seconds (100.00 M allocations: 1.490 GiB, 2.97% gc time)
- Contracts.jl: A different implementation of the Design by Contract paradigm that has very similar syntax and works very well for function contracts up to Julia 0.7.