From b0373d91906a5659e4e78ecec922a155d36db750 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 11 May 2015 17:55:10 +0200
Subject: [PATCH] New benchmarks with strings, justifications, etc..
---
.../purescala/invalid/AsciiToPos.scala | 47 ++++++++++++
.../purescala/valid/TextJustifyNoPost.scala | 75 +++++++++++++++++++
.../verification/editor/AsciiToPos.scala | 47 ++++++++++++
.../editor/TextJustifyNoPost.scala | 75 +++++++++++++++++++
4 files changed, 244 insertions(+)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/AsciiToPos.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/TextJustifyNoPost.scala
create mode 100644 testcases/verification/editor/AsciiToPos.scala
create mode 100644 testcases/verification/editor/TextJustifyNoPost.scala
diff --git a/src/test/resources/regression/verification/purescala/invalid/AsciiToPos.scala b/src/test/resources/regression/verification/purescala/invalid/AsciiToPos.scala
new file mode 100644
index 000000000..4ec536ce7
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/AsciiToPos.scala
@@ -0,0 +1,47 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.lang.string._
+import leon.collection._
+
+object Justify {
+ def tokenize(ascii: List[Char]): List[String] = tokenize0(ascii, "")
+ def tokenize0(ascii: List[Char], wordAcc: String): List[String] = ascii match {
+ case Nil() => Nil()
+ case Cons(h, t) => if (h == ' ') {
+ if (wordAcc.length == 0) {
+ tokenize0(t, wordAcc)
+ } else {
+ Cons(wordAcc, tokenize0(t, ""))
+ }
+ } else {
+ tokenize0(t, String(List(h)) + wordAcc)
+ }
+ }
+
+ def asciiToPos(in: List[Char], index: Int): List[Int] = in match {
+ case Nil() => Nil()
+ case Cons(head, tail) => if(head == ' ') Cons(index, asciiToPos(tail, index+1)) else asciiToPos(tail, index+1)
+ }
+
+ def posToAscii(positions: List[Int], originalText: List[Char], currentPos: Int): List[Char] = positions match {
+ case Cons(start, rest) =>
+ if(start > currentPos) {
+ Cons(' ', posToAscii(rest, originalText, currentPos+1))
+ } else {
+ originalText match {
+ case Cons(l, ls) =>
+ if(l == ' ') {
+ Cons(' ', posToAscii(rest, ls, currentPos+1))
+ } else {
+ Cons(l, posToAscii(positions, ls, currentPos+1))
+ }
+ case Nil() => Nil()
+ }
+ }
+ case Nil() => Nil()
+ }
+
+ def posToAsciiKeepTokens(ascii: List[Char]) = {
+ posToAscii(asciiToPos(ascii, 0), ascii, 0)
+ } ensuring(res => tokenize(res) == tokenize(ascii))
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/TextJustifyNoPost.scala b/src/test/resources/regression/verification/purescala/valid/TextJustifyNoPost.scala
new file mode 100644
index 000000000..e5b06bc94
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/TextJustifyNoPost.scala
@@ -0,0 +1,75 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.collection._
+
+object Justify {
+ /*
+ * The Science of Programming from David Gries Section 20.1
+
+ * The goal is to justify a text. We are given a list of indices corresponding
+ * to the columns of the starting point of each word. Each words are already
+ * separated by one space. The parameter s is the additional number of spaces
+ * at the end of the line that we will need to add between words. We
+ * want the number of space on the same line to differ by at most one.
+ *
+ * If we denote by p and q the two number of spaces between words (p and q differ
+ * only by 1), then we want to only switch once the number of space between words
+ * on the line. This means that we first separate words using p, then we do it using
+ * q until the end of the line.
+ *
+ * z is the line number, the rule is for odd line number to have more spaces on the right (q=p+1)
+ * and for even line number to have more spaces on the left (p=q+1). We do not want trailing
+ * spaces.
+ *
+ * n is the number of words on the line.
+ *
+ * If we apply this justify to each line of a text separately, this should lead to a good looking
+ * justified text.
+
+ * Here is an example:
+ *
+ * justifying lines by
+ * inserting extra blanks is
+ * one task of a text editor.
+ *
+ * results in:
+ *
+ * justifying lines by
+ * inserting extra blanks is
+ * one task of a text editor.
+ */
+
+ def addSpaces(words: List[BigInt], p: BigInt, q: BigInt, t: BigInt, n: BigInt, i: BigInt): List[BigInt] = words match {
+ case Nil() => Nil()
+ case Cons(head, tail) =>
+ if(i <= t) Cons(head + p*(i-1), addSpaces(tail, p, q, t, n, i+1))
+ else if(i > t && i <= n) Cons(head + p*(t-1) + q*(i-t), addSpaces(tail, p, q, t, n, i+1))
+ else Nil() //this should never happen
+ }
+
+ //this version implements the computation of parameters
+ def justifyParamsImpl(n: BigInt, z: BigInt, s: BigInt): (BigInt, BigInt, BigInt) = {
+ require(n >= 2 && s >= 0 && z >= 1)
+ val (q, t, p) = if(z % 2 == 0) {
+ val tmp = s / (n-1)
+ (tmp, 1 + (s % (n - 1)), tmp + 1)
+ } else {
+ val tmp = s / (n-1)
+ (tmp + 1, n - (s % (n - 1)), tmp)
+ }
+ (q, t, p)
+ }
+
+ def justifyImpl(n: BigInt, z: BigInt, s: BigInt, words: List[BigInt]): (BigInt, BigInt, BigInt, List[BigInt]) = {
+ require(n >= 2 && s >= 0 && z >= 1)
+ val (q, t, p) = if(z % 2 == 0) {
+ val tmp = s / (n-1)
+ (tmp, 1 + (s % (n - 1)), tmp + 1)
+ } else {
+ val tmp = s / (n-1)
+ (tmp + 1, n - (s % (n - 1)), tmp)
+ }
+ (q, t, p, addSpaces(words, p, q, t, n, 0))
+ }
+
+}
diff --git a/testcases/verification/editor/AsciiToPos.scala b/testcases/verification/editor/AsciiToPos.scala
new file mode 100644
index 000000000..4ec536ce7
--- /dev/null
+++ b/testcases/verification/editor/AsciiToPos.scala
@@ -0,0 +1,47 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.lang.string._
+import leon.collection._
+
+object Justify {
+ def tokenize(ascii: List[Char]): List[String] = tokenize0(ascii, "")
+ def tokenize0(ascii: List[Char], wordAcc: String): List[String] = ascii match {
+ case Nil() => Nil()
+ case Cons(h, t) => if (h == ' ') {
+ if (wordAcc.length == 0) {
+ tokenize0(t, wordAcc)
+ } else {
+ Cons(wordAcc, tokenize0(t, ""))
+ }
+ } else {
+ tokenize0(t, String(List(h)) + wordAcc)
+ }
+ }
+
+ def asciiToPos(in: List[Char], index: Int): List[Int] = in match {
+ case Nil() => Nil()
+ case Cons(head, tail) => if(head == ' ') Cons(index, asciiToPos(tail, index+1)) else asciiToPos(tail, index+1)
+ }
+
+ def posToAscii(positions: List[Int], originalText: List[Char], currentPos: Int): List[Char] = positions match {
+ case Cons(start, rest) =>
+ if(start > currentPos) {
+ Cons(' ', posToAscii(rest, originalText, currentPos+1))
+ } else {
+ originalText match {
+ case Cons(l, ls) =>
+ if(l == ' ') {
+ Cons(' ', posToAscii(rest, ls, currentPos+1))
+ } else {
+ Cons(l, posToAscii(positions, ls, currentPos+1))
+ }
+ case Nil() => Nil()
+ }
+ }
+ case Nil() => Nil()
+ }
+
+ def posToAsciiKeepTokens(ascii: List[Char]) = {
+ posToAscii(asciiToPos(ascii, 0), ascii, 0)
+ } ensuring(res => tokenize(res) == tokenize(ascii))
+}
diff --git a/testcases/verification/editor/TextJustifyNoPost.scala b/testcases/verification/editor/TextJustifyNoPost.scala
new file mode 100644
index 000000000..e5b06bc94
--- /dev/null
+++ b/testcases/verification/editor/TextJustifyNoPost.scala
@@ -0,0 +1,75 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.collection._
+
+object Justify {
+ /*
+ * The Science of Programming from David Gries Section 20.1
+
+ * The goal is to justify a text. We are given a list of indices corresponding
+ * to the columns of the starting point of each word. Each words are already
+ * separated by one space. The parameter s is the additional number of spaces
+ * at the end of the line that we will need to add between words. We
+ * want the number of space on the same line to differ by at most one.
+ *
+ * If we denote by p and q the two number of spaces between words (p and q differ
+ * only by 1), then we want to only switch once the number of space between words
+ * on the line. This means that we first separate words using p, then we do it using
+ * q until the end of the line.
+ *
+ * z is the line number, the rule is for odd line number to have more spaces on the right (q=p+1)
+ * and for even line number to have more spaces on the left (p=q+1). We do not want trailing
+ * spaces.
+ *
+ * n is the number of words on the line.
+ *
+ * If we apply this justify to each line of a text separately, this should lead to a good looking
+ * justified text.
+
+ * Here is an example:
+ *
+ * justifying lines by
+ * inserting extra blanks is
+ * one task of a text editor.
+ *
+ * results in:
+ *
+ * justifying lines by
+ * inserting extra blanks is
+ * one task of a text editor.
+ */
+
+ def addSpaces(words: List[BigInt], p: BigInt, q: BigInt, t: BigInt, n: BigInt, i: BigInt): List[BigInt] = words match {
+ case Nil() => Nil()
+ case Cons(head, tail) =>
+ if(i <= t) Cons(head + p*(i-1), addSpaces(tail, p, q, t, n, i+1))
+ else if(i > t && i <= n) Cons(head + p*(t-1) + q*(i-t), addSpaces(tail, p, q, t, n, i+1))
+ else Nil() //this should never happen
+ }
+
+ //this version implements the computation of parameters
+ def justifyParamsImpl(n: BigInt, z: BigInt, s: BigInt): (BigInt, BigInt, BigInt) = {
+ require(n >= 2 && s >= 0 && z >= 1)
+ val (q, t, p) = if(z % 2 == 0) {
+ val tmp = s / (n-1)
+ (tmp, 1 + (s % (n - 1)), tmp + 1)
+ } else {
+ val tmp = s / (n-1)
+ (tmp + 1, n - (s % (n - 1)), tmp)
+ }
+ (q, t, p)
+ }
+
+ def justifyImpl(n: BigInt, z: BigInt, s: BigInt, words: List[BigInt]): (BigInt, BigInt, BigInt, List[BigInt]) = {
+ require(n >= 2 && s >= 0 && z >= 1)
+ val (q, t, p) = if(z % 2 == 0) {
+ val tmp = s / (n-1)
+ (tmp, 1 + (s % (n - 1)), tmp + 1)
+ } else {
+ val tmp = s / (n-1)
+ (tmp + 1, n - (s % (n - 1)), tmp)
+ }
+ (q, t, p, addSpaces(words, p, q, t, n, 0))
+ }
+
+}
--
GitLab