3 ms·
Name and functionality inspired by Spec# [0] ... just a bit? Sample Spec# code: int ISqrt(int x) requires 0 <= x; ensures result*result <= x && x < (
by biot 13y ago
Name and functionality inspired by Spec# [0] ... just a bit? Sample Spec# code:
int ISqrt(int x)
requires 0 <= x;
ensures result*result <= x && x < (result+1)*(result+1);
{
int r = 0;
while ((r+1)*(r+1) <= x)
invariant r*r <= x;
{
r++;
}
return r;
}
[0] http://research.microsoft.com/en-us/projects/specsharp/ http://research.microsoft.com/en-us/projects/specsharp/
- farginay 13y agoDifferent thing. Spec# is about embedding specs in your code. Spek appears to be a Behaviour Driven Development (BDD) framework ala RSpec. http://rspec.info/ http://rspec.info/