From 7a27d85a5ad53a8a919a9d0922103b5d7169a069 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 6 Apr 2016 19:44:18 +0200
Subject: [PATCH] shift a list using map with state
---
.../HigherOrderFunctionsMutableParams6.scala | 31 +++++++++++++++++++
1 file changed, 31 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams6.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams6.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams6.scala
new file mode 100644
index 000000000..fcdc822b1
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams6.scala
@@ -0,0 +1,31 @@
+object HigherOrderFunctionsMutableParams6 {
+
+ abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ case class A(var x: BigInt)
+
+ def map(ls: List, f: (BigInt, A) => BigInt, a: A): List = ls match {
+ case Cons(head, tail) =>
+ Cons(f(head, a), map(tail, f, a))
+
+ case Nil() => Nil()
+ }
+
+ def fImpl(el: BigInt, a: A): BigInt = {
+ val last = a.x
+ a.x = el
+ last
+ }
+
+ def shift(ls: List): List = {
+ val a = A(0)
+ map(ls, fImpl, a)
+ }
+
+ def test(): List = {
+ val l = Cons(2, Cons(4, Cons(6, Nil())))
+ shift(l)
+ } ensuring(res => res == Cons(0, Cons(2, Cons(4, Nil()))))
+}
--
GitLab