From 4065074e6d9f135ad9e6de297f0b910e023d169e Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 24 Mar 2011 15:18:42 +0000
Subject: [PATCH]
---
vstte10competition/SumAndMax.scala | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/vstte10competition/SumAndMax.scala b/vstte10competition/SumAndMax.scala
index 2410dff5d..973eb3cf7 100644
--- a/vstte10competition/SumAndMax.scala
+++ b/vstte10competition/SumAndMax.scala
@@ -40,7 +40,8 @@ object SumAndMax {
@induct
def property(list : List) : Boolean = {
- require(allPos(list))
+ // This precondition was given in the problem but isn't actually useful :D
+ // require(allPos(list))
sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
} holds
}
--
GitLab