Menu ▾ ▴

#5 Violated postcondition results in infiltered output, but only the false parts are required

None
new
nobody
None
normal
minor
Always
OCL expressions
2.4.0
2014-12-28
2009-03-13
Lars Hamann
No

Result USE - SVN:

c:\mondexonline\imperative\createExceptionalWorld2.cmd> !opexit
postcondition `WorldDoesNotChange' is false evaluation results:
  self : AbWorld = @world
  self.abAuthPurse : Set(AbPurse) = Set{@abelP,@bankP,@cainP,@newPurse}
  self : AbWorld = @world
  self.abAuthPurse@pre : Set(AbPurse) = Set{@abelP,@bankP,@cainP}
  (self.abAuthPurse = self.abAuthPurse@pre) : Boolean = false
  self : AbWorld = @world
  self.abAuthPurse@pre : Set(AbPurse) = Set{@abelP,@bankP,@cainP}
  purse : AbPurse = @abelP
  purse.coinBalance : Set(Coin) = Set{}
  purse : AbPurse = @abelP
  purse.coinBalance@pre : Set(Coin) = Set{}
  (purse.coinBalance = purse.coinBalance@pre) : Boolean = true
  purse : AbPurse = @abelP
  purse.coinLost : Set(Coin) = Set{}
  purse : AbPurse = @abelP
  purse.coinLost@pre : Set(Coin) = Set{}
  (purse.coinLost = purse.coinLost@pre) : Boolean = true
  ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)) : Boolean = true
  purse : AbPurse = @bankP
  purse.coinBalance : Set(Coin) = Set{@coin1,@coin2}
  purse : AbPurse = @bankP
  purse.coinBalance@pre : Set(Coin) = Set{@coin1,@coin2}
  (purse.coinBalance = purse.coinBalance@pre) : Boolean = true
  purse : AbPurse = @bankP
  purse.coinLost : Set(Coin) = Set{}
  purse : AbPurse = @bankP
  purse.coinLost@pre : Set(Coin) = Set{}
  (purse.coinLost = purse.coinLost@pre) : Boolean = true
  ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)) : Boolean = true
  purse : AbPurse = @cainP
  purse.coinBalance : Set(Coin) = Set{@coin3}
  purse : AbPurse = @cainP
  purse.coinBalance@pre : Set(Coin) = Set{@coin3}
  (purse.coinBalance = purse.coinBalance@pre) : Boolean = true
  purse : AbPurse = @cainP
  purse.coinLost : Set(Coin) = Set{}
  purse : AbPurse = @cainP
  purse.coinLost@pre : Set(Coin) = Set{}
  (purse.coinLost = purse.coinLost@pre) : Boolean = true
  ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)) : Boolean = true
  self.abAuthPurse@pre->forAll(purse : AbPurse | ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre))) : Boolean = true
  ((self.abAuthPurse = self.abAuthPurse@pre) and self.abAuthPurse@pre->forAll(purse : AbPurse | ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)))) : Boolean = false
c:\mondexonline\imperative\createExceptionalWorld2.cmd>
use>

Discussion

  • Frank

    Frank - 2014-09-19
    • Description has changed:

    Diff:

    --- old
+++ new
@@ -1,46 +1,50 @@
-Result USE \- SVN:
+Result USE - SVN:

-c:\\mondexonline\\imperative\\createExceptionalWorld2\.cmd> \!opexit postcondition \`WorldDoesNotChange' is false evaluation results:
-&nbps; self : AbWorld = @world
-&nbps; self\.abAuthPurse : Set\(AbPurse\) = Set\{@abelP,@bankP,@cainP,@newPurse\}
-&nbps; self : AbWorld = @world
-&nbps; self\.abAuthPurse@pre : Set\(AbPurse\) = Set\{@abelP,@bankP,@cainP\}
-&nbps; \(self\.abAuthPurse = self\.abAuthPurse@pre\) : Boolean = false
-&nbps; self : AbWorld = @world
-&nbps; self\.abAuthPurse@pre : Set\(AbPurse\) = Set\{@abelP,@bankP,@cainP\}
-&nbps; purse : AbPurse = @abelP
-&nbps; purse\.coinBalance : Set\(Coin\) = Set\{\}
-&nbps; purse : AbPurse = @abelP
-&nbps; purse\.coinBalance@pre : Set\(Coin\) = Set\{\}
-&nbps; \(purse\.coinBalance = purse\.coinBalance@pre\) : Boolean = true
-&nbps; purse : AbPurse = @abelP
-&nbps; purse\.coinLost : Set\(Coin\) = Set\{\}
-&nbps; purse : AbPurse = @abelP
-&nbps; purse\.coinLost@pre : Set\(Coin\) = Set\{\}
-&nbps; \(purse\.coinLost = purse\.coinLost@pre\) : Boolean = true
-&nbps; \(\(purse\.coinBalance = purse\.coinBalance@pre\) and \(purse\.coinLost = purse\.coinLost@pre\)\) : Boolean = true
-&nbps; purse : AbPurse = @bankP
-&nbps; purse\.coinBalance : Set\(Coin\) = Set\{@coin1,@coin2\}
-&nbps; purse : AbPurse = @bankP
-&nbps; purse\.coinBalance@pre : Set\(Coin\) = Set\{@coin1,@coin2\}
-&nbps; \(purse\.coinBalance = purse\.coinBalance@pre\) : Boolean = true
-&nbps; purse : AbPurse = @bankP
-&nbps; purse\.coinLost : Set\(Coin\) = Set\{\}
-&nbps; purse : AbPurse = @bankP
-&nbps; purse\.coinLost@pre : Set\(Coin\) = Set\{\}
-&nbps; \(purse\.coinLost = purse\.coinLost@pre\) : Boolean = true
-&nbps; \(\(purse\.coinBalance = purse\.coinBalance@pre\) and \(purse\.coinLost = purse\.coinLost@pre\)\) : Boolean = true
-&nbps; purse : AbPurse = @cainP
-&nbps; purse\.coinBalance : Set\(Coin\) = Set\{@coin3\}
-&nbps; purse : AbPurse = @cainP
-&nbps; purse\.coinBalance@pre : Set\(Coin\) = Set\{@coin3\}
-&nbps; \(purse\.coinBalance = purse\.coinBalance@pre\) : Boolean = true
-&nbps; purse : AbPurse = @cainP
-&nbps; purse\.coinLost : Set\(Coin\) = Set\{\}
-&nbps; purse : AbPurse = @cainP
-&nbps; purse\.coinLost@pre : Set\(Coin\) = Set\{\}
-&nbps; \(purse\.coinLost = purse\.coinLost@pre\) : Boolean = true
-&nbps; \(\(purse\.coinBalance = purse\.coinBalance@pre\) and \(purse\.coinLost = purse\.coinLost@pre\)\) : Boolean = true
-&nbps; self\.abAuthPurse@pre\->forAll\(purse : AbPurse | \(\(purse\.coinBalance = purse\.coinBalance@pre\) and \(purse\.coinLost = purse\.coinLost@pre\)\)\) : Boolean = true
-&nbps; \(\(self\.abAuthPurse = self\.abAuthPurse@pre\) and self\.abAuthPurse@pre\->forAll\(purse : AbPurse | \(\(purse\.coinBalance = purse\.coinBalance@pre\) and \(purse\.coinLost = purse\.coinLost@pre\)\)\)\) : Boolean = false c:\\mondexonline\\imperative\\createExceptionalWorld2\.cmd>
-use>
+~~~~~
+c:\mondexonline\imperative\createExceptionalWorld2.cmd> !opexit
+postcondition `WorldDoesNotChange' is false evaluation results:
+  self : AbWorld = @world
+  self.abAuthPurse : Set(AbPurse) = Set{@abelP,@bankP,@cainP,@newPurse}
+  self : AbWorld = @world
+  self.abAuthPurse@pre : Set(AbPurse) = Set{@abelP,@bankP,@cainP}
+  (self.abAuthPurse = self.abAuthPurse@pre) : Boolean = false
+  self : AbWorld = @world
+  self.abAuthPurse@pre : Set(AbPurse) = Set{@abelP,@bankP,@cainP}
+  purse : AbPurse = @abelP
+  purse.coinBalance : Set(Coin) = Set{}
+  purse : AbPurse = @abelP
+  purse.coinBalance@pre : Set(Coin) = Set{}
+  (purse.coinBalance = purse.coinBalance@pre) : Boolean = true
+  purse : AbPurse = @abelP
+  purse.coinLost : Set(Coin) = Set{}
+  purse : AbPurse = @abelP
+  purse.coinLost@pre : Set(Coin) = Set{}
+  (purse.coinLost = purse.coinLost@pre) : Boolean = true
+  ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)) : Boolean = true
+  purse : AbPurse = @bankP
+  purse.coinBalance : Set(Coin) = Set{@coin1,@coin2}
+  purse : AbPurse = @bankP
+  purse.coinBalance@pre : Set(Coin) = Set{@coin1,@coin2}
+  (purse.coinBalance = purse.coinBalance@pre) : Boolean = true
+  purse : AbPurse = @bankP
+  purse.coinLost : Set(Coin) = Set{}
+  purse : AbPurse = @bankP
+  purse.coinLost@pre : Set(Coin) = Set{}
+  (purse.coinLost = purse.coinLost@pre) : Boolean = true
+  ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)) : Boolean = true
+  purse : AbPurse = @cainP
+  purse.coinBalance : Set(Coin) = Set{@coin3}
+  purse : AbPurse = @cainP
+  purse.coinBalance@pre : Set(Coin) = Set{@coin3}
+  (purse.coinBalance = purse.coinBalance@pre) : Boolean = true
+  purse : AbPurse = @cainP
+  purse.coinLost : Set(Coin) = Set{}
+  purse : AbPurse = @cainP
+  purse.coinLost@pre : Set(Coin) = Set{}
+  (purse.coinLost = purse.coinLost@pre) : Boolean = true
+  ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)) : Boolean = true
+  self.abAuthPurse@pre->forAll(purse : AbPurse | ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre))) : Boolean = true
+  ((self.abAuthPurse = self.abAuthPurse@pre) and self.abAuthPurse@pre->forAll(purse : AbPurse | ((purse.coinBalance = purse.coinBalance@pre) and (purse.coinLost = purse.coinLost@pre)))) : Boolean = false
+c:\mondexonline\imperative\createExceptionalWorld2.cmd>
+use>
+~~~~~
    • assigned_to: Frank
    • Milestone: --> None
    • Reproducibility: always --> Always
     

  • Frank

    Frank - 2014-09-19
    • assigned_to: Frank --> nobody
     

Log in to post a comment.

Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.