From 1178be3d695dfe905242e882698a05e98e094859 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 4 Feb 2013 14:16:19 +0100
Subject: [PATCH] Completes Justify testcase
This commit completes the Justify testcase with some more
advanced properties.
It provides both an implementation with its specification for
verification, and a synthesis benchmark where choose is used
to try to derive the correct implementation.
---
testcases/synthesis/Justify.scala | 80 +++++++++++++++++++++++++++++--
1 file changed, 77 insertions(+), 3 deletions(-)
diff --git a/testcases/synthesis/Justify.scala b/testcases/synthesis/Justify.scala
index 2c3ff9a32..cc0227115 100644
--- a/testcases/synthesis/Justify.scala
+++ b/testcases/synthesis/Justify.scala
@@ -46,8 +46,8 @@ object Justify {
//here p and q are as defined above. t is used to find the index of the word where
//we switch from p spaces to q spaces.
- val (res, p, q, t) = choose((justifiedWords: IntList, p: Int, q: Int, t: Int) =>
- p >= 0 && q >= 0 && p == q+1 && t >= 1 && t <= n &&
+ val (res, p, q, t) = choose((justifiedWords: IntList, p: Int, q: Int, t: Int) =>
+ p >= 0 && q >= 0 && t >= 1 && t <= n &&
p*(t-1) + q*(n-t) == s && //this constraint is probably going to be an issue since it is non linear
((z % 2 == 1 && q == p + 1) || (z % 2 == 0 && p == q + 1)) &&
justifiedWords == addSpaces(words, p, q, t, n, 0) //this is likely to be problematic as well
@@ -64,6 +64,41 @@ object Justify {
else IntNil() //this should never happen
}
+ //this version implements the computation of parameters
+ def justifyParamsImpl(n: Int, z: Int, s: Int): (Int, Int, Int) = {
+ 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)
+ } ensuring(res => {
+ val (q, t, p) = res
+ p >= 0 && q >= 0 && t >= 1 && t <= n && p*(t - 1) + q*(n-t) == s &&
+ ((z % 2 == 1 && q == p + 1) || (z % 2 == 0 && p == q + 1))
+ })
+
+ def justifyImpl(n: Int, z: Int, s: Int, words: IntList): (Int, Int, Int, IntList) = {
+ 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))
+ } ensuring(res => {
+ val (q, t, p, justifiedWords) = res
+ p >= 0 && q >= 0 && t >= 1 && t <= n &&
+ p*(t-1) + q*(n-t) == s && //this constraint is probably going to be an issue since it is non linear
+ ((z % 2 == 1 && q == p + 1) || (z % 2 == 0 && p == q + 1)) &&
+ justifiedWords == addSpaces(words, p, q, t, n, 0) //this is likely to be problematic as well
+ })
+
/*
* This version is a simpler one, in which we are just trying to determine parameters that can then
* be mecanically used to build the justified text. Also we do not distinguish on even/odd line number.
@@ -71,11 +106,50 @@ object Justify {
def simpleJustify(n: Int, z: Int, s: Int, words: IntList): (Int, Int, Int) = {
require(n >= 0 && s >= 0 && z >= 1)
- val (p, q, t) = choose((p: Int, q: Int, t: Int) =>
+ val (p, q, t) = choose((p: Int, q: Int, t: Int) =>
p >= 0 && q >= 0 && p == q+1 && t >= 1 && t <= n && p*(t - 1) + q*(n-t) == s
)
//actually, we could simply use the parameter to program the ocnstruction of the List, rather than explicitly synthesizing it
(p, q, t)
}
+
+ //we use ascii code to represent text, 32 is the space separator
+ case class Word(chars: IntList)
+
+ abstract class WordList
+ case class WordCons(word: IntList, tail: WordList) extends WordList
+ case class WordNil() extends WordList
+
+ def tokenize(ascii: IntList): WordList = tokenize0(ascii, IntNil())
+ def tokenize0(ascii: IntList, wordAcc: IntList): WordList = ascii match {
+ case IntNil() => WordNil()
+ case IntCons(head, tail) => if(head == 32) (wordAcc match {
+ case IntNil() => tokenize0(tail, IntNil())
+ case IntCons(l, ls) => WordCons(wordAcc, tokenize0(tail, IntNil()))
+ }) else tokenize0(tail, IntCons(head, wordAcc))
+ }
+
+
+ //we assume only one space between each word. This is the assumption made
+ //in the representation used in the previous algorithm
+
+ def asciiToPos(in: IntList, index: Int): IntList = in match {
+ case IntNil() => IntNil()
+ case IntCons(head, tail) => if(head == 32) IntCons(index, asciiToPos(tail, index+1)) else asciiToPos(tail, index+1)
+ }
+
+ def posToAscii(positions: IntList, originalText: IntList, currentPos: Int): IntList = positions match {
+ case IntCons(start, rest) => if(start > currentPos) IntCons(32, posToAscii(rest, originalText, currentPos+1)) else
+ (originalText match {
+ case IntCons(l, ls) => if(l == 32) IntCons(32, posToAscii(rest, ls, currentPos+1)) else IntCons(l, posToAscii(positions, ls, currentPos+1))
+ case IntNil() => IntNil()
+ })
+ case IntNil() => IntNil()
+ }
+
+ def posToAsciiKeepTokens(ascii: IntList) = {
+ posToAscii(asciiToPos(ascii, 0), ascii, 0)
+ } ensuring(res => tokenize(res) == tokenize(ascii))
+
}
--
GitLab