aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorIvan Enderlin <ivan.enderlin@hoa-project.net>2013-11-01 17:35:06 +0100
committerIvan Enderlin <ivan.enderlin@hoa-project.net>2013-11-01 17:44:12 +0100
commit668326817446f5ab843f36004014f3cb22fe9657 (patch)
treed17ed95458902530c0e41cec8e291caf31efb61f
parentc4f955afb4014ff8c4a302ef1ea82afa2d8d708d (diff)
downloadPraspel-668326817446f5ab843f36004014f3cb22fe9657.zip
Praspel-668326817446f5ab843f36004014f3cb22fe9657.tar.gz
Praspel-668326817446f5ab843f36004014f3cb22fe9657.tar.bz2
Add trace support!
Just give a Hoa\Praspel\Trace object in the Hoa\Praspel::evaluate() method, and use the Hoa\Praspel\Visitor\Praspel to print it!
-rw-r--r--Praspel.php112
-rw-r--r--Trace.php62
2 files changed, 155 insertions, 19 deletions
diff --git a/Praspel.php b/Praspel.php
index 0aa3a03..63e9182 100644
--- a/Praspel.php
+++ b/Praspel.php
@@ -74,6 +74,11 @@ from('Hoa')
-> import('Praspel.Exception.Failure.InternalPrecondition')
/**
+ * \Hoa\Praspel\Trace
+ */
+-> import('Praspel.Trace')
+
+/**
* \Hoa\Praspel\Visitor\Interpreter
*/
-> import('Praspel.Visitor.Interpreter')
@@ -170,11 +175,12 @@ class Praspel {
* Runtime assertion checker.
*
* @access public
+ * @param \Hoa\Praspel\Trace $trace Trace.
* @return bool
* @throw \Hoa\Praspel\Exception\Generic
* @throw \Hoa\Praspel\Exception\Group
*/
- public function evaluate ( ) {
+ public function evaluate ( &$trace = false ) {
// Start.
$verdict = true;
@@ -188,6 +194,9 @@ class Praspel {
if($reflection instanceof \ReflectionMethod)
$reflection->setAccessible(true);
+ if(false !== $trace && !($trace instanceof Trace))
+ $trace = new Trace();
+
// Prepare data.
if(null === $data = $this->getData())
if(true === $this->canGenerateData())
@@ -225,7 +234,8 @@ class Praspel {
$arguments,
$exceptions,
__NAMESPACE__ . '\Exception\Failure\Invariant',
- true
+ true,
+ $trace
);
if(0 < count($exceptions))
@@ -238,7 +248,8 @@ class Praspel {
$behavior,
$arguments,
$exceptions,
- true
+ true,
+ $trace
);
if(0 < count($exceptions))
@@ -280,7 +291,9 @@ class Praspel {
$ensures,
$arguments,
$_exceptions,
- __NAMESPACE__ . '\Exception\Failure\Postcondition'
+ __NAMESPACE__ . '\Exception\Failure\Postcondition',
+ false,
+ $trace
);
}
@@ -333,7 +346,8 @@ class Praspel {
$arguments,
$exceptions,
__NAMESPACE__ . '\Exception\Failure\Invariant',
- true
+ true,
+ $trace
);
if(0 < count($exceptions))
@@ -347,18 +361,20 @@ class Praspel {
* Check behavior clauses.
*
* @access protected
- * @param \Hoa\Praspel\Model\Behavior &$behavior Behavior clause.
+ * @param \Hoa\Praspel\Model\Behavior $behavior Behavior clause.
* @param array &$data Data.
* @param \Hoa\Praspel\Exception\Group $exceptions Exceptions group.
* @param bool $assign Assign data to
* variable.
+ * @param \Hoa\Praspel\Trace $trace Trace.
* @return bool
* @throw \Hoa\Praspel\Exception
*/
- protected function checkBehavior ( Model\Behavior &$behavior,
+ protected function checkBehavior ( Model\Behavior $behavior,
Array &$data,
Exception\Group $exceptions,
- $assign = false ) {
+ $assign = false,
+ $trace = false ) {
$verdict = true;
@@ -371,7 +387,8 @@ class Praspel {
$data,
$exceptions,
__NAMESPACE__ . '\Exception\Failure\Precondition',
- $assign
+ $assign,
+ $trace
);
if(false === $verdict)
@@ -389,19 +406,34 @@ class Praspel {
$_exceptions = new Exception\Group(
'Behavior %s is broken.',
- 4, $_behavior->getIdentifier());
+ 6, $_behavior->getIdentifier()
+ );
+
+ $_trace = null;
+
+ if(!empty($trace)) {
+
+ $_trace = new Model\Behavior($trace);
+ $_trace->setIdentifier($_behavior->getIdentifier());
+ }
$_verdict = $this->checkBehavior(
$_behavior,
$data,
$_exceptions,
- $assign
+ $assign,
+ $_trace
);
- if(true === $_verdict)
+ if(true === $_verdict) {
+
+ $trace->addClause($_trace);
+
break;
+ }
$exceptions[] = $_exceptions;
+ unset($_trace);
}
if(false === $_verdict) {
@@ -438,14 +470,20 @@ class Praspel {
* throw.
* @param bool $assign Assign data to
* variable.
+ * @param \Hoa\Praspel\Trace $trace Trace.
* @return bool
* @throw \Hoa\Praspel\Exception
*/
protected function checkClause ( Model\Declaration $clause, Array &$data,
Exception\Group $exceptions, $exception,
- $assign = false ) {
+ $assign = false,
+ $trace = false ) {
- $verdict = true;
+ $verdict = true;
+ $traceClause = null;
+
+ if(!empty($trace))
+ $traceClause = clone $clause;
foreach($clause as $name => $variable) {
@@ -462,10 +500,33 @@ class Praspel {
continue;
}
- $datum = &$data[$_name];
- $_verdict = $variable->predicate($datum);
+ $datum = &$data[$_name];
+ $_verdict = false;
+ $traceVariable = null;
+
+ if(null !== $traceClause) {
+
+ $traceVariable = clone $variable;
+ $traceVariableDomains = $traceVariable->getDomains();
+ }
+
+ $i = 0;
+
+ foreach($variable->getDomains() as $realdom) {
+
+ if(false === $_verdict && true === $realdom->predicate($datum))
+ $_verdict = true;
+ else
+ unset($traceVariableDomains[$i--]);
+
+ ++$i;
+ }
+
+ if(false === $_verdict) {
+
+ if(null !== $traceClause)
+ unset($traceClause[$name]);
- if(false === $_verdict)
$exceptions[] = new $exception(
'Variable %s does not verify the constraint @%s %s.',
6,
@@ -474,12 +535,25 @@ class Praspel {
$clause->getName(),
$this->getVisitorPraspel()->visit($variable)
));
- elseif(true === $assign)
- $variable->setValue($datum);
+ }
+ else {
+
+ if(true === $assign)
+ $variable->setValue($datum);
+
+ if(null !== $traceClause) {
+
+ unset($traceClause[$name]);
+ $traceClause->addVariable($name, $traceVariable);
+ }
+ }
$verdict &= $_verdict;
}
+ if(!empty($trace))
+ $trace->addClause($traceClause);
+
return (bool) $verdict;
}
diff --git a/Trace.php b/Trace.php
new file mode 100644
index 0000000..6d5da1c
--- /dev/null
+++ b/Trace.php
@@ -0,0 +1,62 @@
+<?php
+
+/**
+ * Hoa
+ *
+ *
+ * @license
+ *
+ * New BSD License
+ *
+ * Copyright © 2007-2013, Ivan Enderlin. All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * * Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ * * Neither the name of the Hoa nor the names of its contributors may be
+ * used to endorse or promote products derived from this software without
+ * specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS AND CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ */
+
+namespace {
+
+from('Hoa')
+
+/**
+ * \Hoa\Praspel\Model\Specification
+ */
+-> import('Praspel.Model.Specification');
+
+}
+
+namespace Hoa\Praspel {
+
+/**
+ * Class \Hoa\Praspel\Trace.
+ *
+ * A trace is a derivated specification.
+ *
+ * @author Ivan Enderlin <ivan.enderlin@hoa-project.net>
+ * @copyright Copyright © 2007-2013 Ivan Enderlin.
+ * @license New BSD License
+ */
+
+class Trace extends Model\Specification { }
+
+}