DesignByContract.jl

Description

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.

Installation

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

Usage

DesignByContract.jl works by processing a block containing the prerequisites, post-conditions and the contract’s function.

Prerequisites

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
end

putItem! (generic function with 1 method)

fruits = Dict{String, Any}()

putItem!(fruits, "apple", :red)
fruits

Dict{String,Any} with 1 entry:
  "apple" => :red

putItem!(fruits, "blueberry", :blue)
fruits

Dict{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

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
end

incrArr! (generic function with 1 method)

arr = collect(1:5)
display(arr)
incrArr!(arr)
arr

5-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)
arr

5-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)
arr

5-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

Return contract

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
end

processArr (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

Return name

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
end

newProcessArr (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

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
end

quote
    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.

Check Disabling

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)

Related Packages

• 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.

TODOs

[X] Add loop invariant

[X] Add functionality

[X] Test Loop invariants

[X] Add README entry

[ ] Add old value call

[ ] Add Agreement

[ ] Add README entry

[X] Enable assertion disabling for efficiency

[X] Add DocStrings