aboutsummaryrefslogtreecommitdiffstats
path: root/Model/Variable
diff options
context:
space:
mode:
authorIvan Enderlin <ivan.enderlin@hoa-project.net>2013-11-11 09:07:10 +0100
committerIvan Enderlin <ivan.enderlin@hoa-project.net>2013-11-11 09:07:10 +0100
commitbec521d2cfc22274213ac5066d8817a085faa316 (patch)
treea4d6db99463882b16840039a94e1327ad9f8fe23 /Model/Variable
parent6e854e85824bc3af64236912ec0e336d9d6315bc (diff)
downloadPraspel-bec521d2cfc22274213ac5066d8817a085faa316.zip
Praspel-bec521d2cfc22274213ac5066d8817a085faa316.tar.gz
Praspel-bec521d2cfc22274213ac5066d8817a085faa316.tar.bz2
Support dynamic resolutions as external variables.
`this->foo` is considered as a borrowing variable, with the type `TYPE_EXTERNAL`. Verifications use the contract registry and the binded class of specifications.
Diffstat (limited to 'Model/Variable')
-rw-r--r--Model/Variable/Borrowing.php125
1 files changed, 104 insertions, 21 deletions
diff --git a/Model/Variable/Borrowing.php b/Model/Variable/Borrowing.php
index 6f9268e..4400fab 100644
--- a/Model/Variable/Borrowing.php
+++ b/Model/Variable/Borrowing.php
@@ -69,7 +69,14 @@ class Borrowing extends Variable {
*
* @const int
*/
- const TYPE_OLD = 1;
+ const TYPE_OLD = 0;
+
+ /**
+ * Type: external (e.g. this->foo->bar).
+ *
+ * @const int
+ */
+ const TYPE_EXTERNAL = 1;
/**
* Type.
@@ -115,34 +122,110 @@ class Borrowing extends Variable {
*/
protected function determineType ( ) {
- $name = $this->getName();
+ $name = $this->getName();
+
+ if('\old(' === substr($name, 0, 5))
+ $this->computeOld(substr($name, 5, -1));
+ elseif(false !== strpos($name, '>', 2))
+ $this->computeDynamicResolution($name);
+ else
+ throw new \Hoa\Praspel\Exception\Model(
+ 'Variable %s would be a borrowing one, but its type cannot ' .
+ 'be determined.', 0, $name);
+
+ return;
+ }
+
+ /**
+ * Compute \old(…).
+ *
+ * @access protected
+ * @param string $name Name.
+ * @return void
+ * @throw \Hoa\Praspel\Exception\Model
+ */
+ protected function computeOld ( $name ) {
+
+ $clause = $this->getClause();
+ $this->_type = static::TYPE_OLD;
+ $parent = $clause->getParent();
+
+ while( false === $parent->clauseExists('requires')
+ && null !== $parent = $parent->getParent());
+
+ if( null === $parent
+ || false === $parent->clauseExists('requires'))
+ throw new \Hoa\Praspel\Exception\Model(
+ 'No parent or no requires.', 1);
+
+ $requires = $parent->getClause('requires');
+ $inScopeVariables = $requires->getInScopeVariables();
+
+ if(!isset($inScopeVariables[$name]))
+ throw new \Hoa\Praspel\Exception\Model(
+ 'Variable %s does not exist, cannot get its old value ' .
+ '(in @%s).',
+ 2, array($name, $clause->getName()));
+
+ $this->_variable = &$inScopeVariables[$name];
+
+ return;
+ }
+
+ /**
+ * Compute dynamic resolution.
+ *
+ * @access protected
+ * @param string $name Name.
+ * @return void
+ * @throw \Hoa\Praspel\Exception\Model
+ */
+ protected function computeDynamicResolution ( $name ) {
+
+ $this->_type = static::TYPE_EXTERNAL;
+
$clause = $this->getClause();
+ $parts = explode('->', $name);
+ $head = array_shift($parts);
+
+ if('this' !== $head)
+ //$head = $clause->getVariable($parts[0]);
+ throw new \Hoa\Praspel\Exception\Model('Not yet implemented!');
+
+ $registry = \Hoa\Praspel::getRegistry();
+ $root = $clause->getRoot();
+ $bindedClass = $root->getBindedClass();
+
+ if(null === $bindedClass)
+ throw new \Hoa\Praspel\Exception\Model(
+ 'Cannot resolve the dynamic identifier %s; ' .
+ '%s::getBindedClass returned null.',
+ 3, array($name, get_class($root)));
- if('\old(' === substr($name, 0, 5)) {
+ $attribute = array_shift($parts);
+ $id = $bindedClass . '::$' . $attribute;
- $this->_type = static::TYPE_OLD;
- $old = substr($name, 5, -1);
- $parent = $clause->getParent();
+ if(!isset($registry[$id]))
+ throw new \Hoa\Praspel\Exception\Model(
+ 'The identifier contract %s does not exist in the registry.',
+ 4, $name);
- while( false === $parent->clauseExists('requires')
- && null !== $parent = $parent->getParent());
+ $entry = $registry[$id];
- if( null === $parent
- || false === $parent->clauseExists('requires'))
- throw new \Hoa\Praspel\Exception\Model(
- 'No parent or no requires.', 0);
+ if(false === $entry->clauseExists('invariant'))
+ throw new \Hoa\Praspel\Exception\Model(
+ '%s is not declared with an @invariant clause.',
+ 5, $id);
- $requires = $parent->getClause('requires');
- $inScopeVariables = $requires->getInScopeVariables();
+ $targetedClause = $entry->getClause('invariant');
- if(!isset($inScopeVariables[$old]))
- throw new \Hoa\Praspel\Exception\Model(
- 'Variable %s does not exist, cannot get its old value ' .
- '(in @%s).',
- 1, array($old, $clause->getName()));
+ if(!isset($targetedClause[$attribute]))
+ throw new \Hoa\Praspel\Exception\Model(
+ 'The identifier %s does not exist.',
+ 6, $attribute);
- $this->_variable = &$inScopeVariables[$old];
- }
+ $variable = $targetedClause[$attribute];
+ $this->_variable = $variable;
return;
}