Exist the type bouble or decimal??

Jun 13, 2014 at 4:45 PM
I can not represent the type decimal or double? I want to try a method that calculates the mean and standard deviation but misses me with integer type.


Jun 16, 2014 at 7:01 PM
You can use "real".

Jun 17, 2014 at 6:02 PM
Leino, thanks for your response. However, I fail to cast the result. If i change the sentence: m:= real(z / a.Length) dafny returns that function calls are allowed only in specification contexts. Why?

method mean (a: array<int>) returns (m: real)
requires a != null && a.Length > 0;
var z:= 0;
var i:= 0;
while(i < a.Length)
invariant 0 <= i <= a.Length;
z := z + a[i];
i := i + 1;
m:= (z / a.Length);
Jun 17, 2014 at 9:48 PM
Whoa! That's a bug. I shall fix it. Thanks for reporting it. (In the meantime, if you don't care about executing your program, you can declare the method as a "ghost method" as a temporary solution.)

Jun 30, 2014 at 6:08 PM
Thanks Leino. You can notify me when the bug has been fixed??
Jul 10, 2014 at 11:44 PM
Hi Silvana,

Thanks for your patience. The bug has now been fixed (in change set 08206907cdff). Please let me know of any other problems. Thanks.

Marked as answer by rustanleino on 9/9/2014 at 11:58 AM