Design an embedded DSL to express pre/post conditions
Constructs that have to be supported:
- Simple logic expressions
- Quantifiers
- ... (other constructs?)
Discussed idea
- Quantifiers could be expressions as a function taking a lambda that returns a simple expression
Idea by Wishu
Example specifying "swap"
class Swap {
void swap(a,k,i) { .... implementation of a method to swap a[k] and a[i] }
boolean swap_spec (a,k,i) {
// introducing vars to remember old values
oldak = a[k] ; oldai = a[i] ;
assert a!=null && a.length > 0 && k>=0 && i>=0 ;
swap(a,k,i) ;
assert (a[k]=oldai) && (a[i]==oldak) ;
}
}Example specifying a program to get the maximum value of an array
class Max {
int getMax(int[] a) { .... implementation of a method to calculate the greatest element of the array a
getMax_spec(int[] a) {
assert a!=null && a.length > 0 ;
int retval = getMax(a) ;
assert exists(a, x -> x == retval ) && forall(a, x -> x <= retval) ;
}
}