Syntax options

[zenna]

The interface to spec has many possible alternatives:

f(x) = abs(x)
@post f(ret, x) = x > 0
@post f(ret, x) = typeof(x) == typeof(0)

The nice thing about this is that it's explicit, but it's a bit verbose as I have to keep repeating the function arguments The other problem is that I would need to figure out how to make sure these two specs are different and one doesn't overwrite the other but instead we get a conjunction.

@post begin
function f(x)
  abs(x)
end
x > 0
end

@pre sort!(x::Vector{Int}) = length(x) > 3
@capture sort!(x) = (x = deepcopy(x))
@post sort!(cap, ret, x) = ret == sort(cap.x)

function sort(x
   ...
end
pre length(x) > 0
capture > 0
post x > 0

Or, we have a macro for last method

f(x) = abs(x)
@post f x > 0
@post f typeof(x) == typeof(0)

This is nice, maybe the best we can do