aboutsummaryrefslogtreecommitdiffstats
path: root/AssertionChecker
diff options
context:
space:
mode:
authorIvan Enderlin <ivan.enderlin@hoa-project.net>2014-03-31 17:18:55 +0200
committerIvan Enderlin <ivan.enderlin@hoa-project.net>2014-03-31 17:18:55 +0200
commitcc375fb2fd341d1165077cd0151bc0cbd1fea88b (patch)
tree335c4a96288e2aa6fdbe95d9bdf578ca1e378d13 /AssertionChecker
parent7cab3a4bbf34e16eda7e6d4f725c6a72d8d7619c (diff)
downloadPraspel-cc375fb2fd341d1165077cd0151bc0cbd1fea88b.zip
Praspel-cc375fb2fd341d1165077cd0151bc0cbd1fea88b.tar.gz
Praspel-cc375fb2fd341d1165077cd0151bc0cbd1fea88b.tar.bz2
Absent @ensures => failed.
Diffstat (limited to 'AssertionChecker')
-rw-r--r--AssertionChecker/Runtime.php31
1 files changed, 22 insertions, 9 deletions
diff --git a/AssertionChecker/Runtime.php b/AssertionChecker/Runtime.php
index 4077bd0..e96b6ce 100644
--- a/AssertionChecker/Runtime.php
+++ b/AssertionChecker/Runtime.php
@@ -216,16 +216,17 @@ class Runtime extends AssertionChecker {
);
$arguments['\result'] = $return;
+ $rootBehavior = $behavior instanceof \Hoa\Praspel\Model\Specification;
+ $_exceptions = true === $rootBehavior
+ ? $exceptions
+ : new \Hoa\Praspel\Exception\Group(
+ 'Behavior %s is broken.',
+ 3, $behavior->getIdentifier()
+ );
+
// Check normal postcondition.
if(true === $behavior->clauseExists('ensures')) {
- $_exceptions = $behavior instanceof \Hoa\Praspel\Model\Specification
- ? $exceptions
- : new \Hoa\Praspel\Exception\Group(
- 'Behavior %s is broken.',
- 3, $behavior->getIdentifier()
- );
-
$ensures = $behavior->getClause('ensures');
$verdict &= $this->checkClause(
$ensures,
@@ -235,6 +236,19 @@ class Runtime extends AssertionChecker {
false,
$trace
);
+ }
+ else {
+
+ $verdict &= false;
+ $_exceptions[] = new \Hoa\Praspel\Exception\Failure\Postcondition(
+ 'The System Under Test cannot terminate normally because ' .
+ 'no normal postcondition has been specified (there is ' .
+ 'no @ensures clause).', 3);
+ }
+
+ if( 0 < count($_exceptions)
+ && false === $rootBehavior) {
+
$_behavior = $behavior;
while( (null !== $_behavior = $_behavior->getParent())
@@ -248,8 +262,7 @@ class Runtime extends AssertionChecker {
$_exceptions = $handle;
}
- if(0 < count($_exceptions))
- $exceptions[] = $_exceptions;
+ $exceptions[] = $_exceptions;
}
}
catch ( \Hoa\Praspel\Exception $internalException ) {