Are the following two OCL statements equivalent for some function context?
post: if a > 0 then b < c
post: b < c implies a > 0
Equivalence of if-then and implies in OCL statements
557 Views Asked by a_fan At
1
There are 1 best solutions below
Related Questions in OCL
- Merge Project models through EML using complex comparison rules
- get "SAXSparseEception: Content is not allowed in prolog" when parsing an OCL file in my Eclipse plugin
- UML constraint {xor} between two associations
- Validate OCL attributes of my model using Eclipse papyrus
- Object Constraint Language (OCL) syntax checker
- Generate Java Code from OCLInEcore in MWE2 Workflow
- Write OCL restrictions related to associations with other classes
- Representing QVT-Operational transformations in XML, JSON or or any other serialized format
- OCL - Composition relation, can it be referenced backwards?
- How can I add OCL restriction to the class variable?
- Can you use dot notation when referring to classes in relation to other classes in OCL?
- How do I find a UML object if I only know the value of one of its attributes in OCL?
- Get ocl string attribute length
- Understanding the semantics of some OCL operands
- How to use MDriven OclPs to find all objects matching a list of strings?
Related Questions in FORMAL-METHODS
- VSCoq Error: Connection to server got closed. Server will not be restarted
- How to make Spoq generate high-level specifications in Coq (not just AST) for the functions in LLVM IR
- UPPAAL chooses to loop on instead of a transition of a higher priority
- Dafny verification fails "post condition might not hold"
- How to capture a change in an element of an array in TLA+
- how to solve the undetermined issue in a let-such-that expression in Dafny?
- Term for statements with vacuous weakest precondition
- VECTORSZ size is too small in ispin
- Using the B-Method for structured data verification
- No Instance Found on integer declaration greater than 7
- error FS0001: This expression was expected to have type 'cexp' but here has type 'Label'
- Z notation specification to modify content of a set
- Atelier B - Proving simple PO in the context of a loop
- Atelier B - Proof obligations of "H => vv$1 = vv$2" format for vv used in WHILE substitution
- How to rank solutions using SMT solver like Z3 in formal logic
Related Questions in POST-CONDITIONS
- Dafny method will not verify
- Dafny Method to find Max fails to verify
- program written in dafny, implementing the Merge Sorted Arrays in-Place algorithm
- Sort and switch methods in Dafny (Invariants error)
- Neo4js conditional information storage
- Weak precondition and strong postcondition problems?
- (Dafny) Postcondition might not hold when filtering vowels
- Strengthening and Weakening of pre and post conditions
- Equivalence of if-then and implies in OCL statements
- Find inputs to a function which break the postcondition on the output
- How can i assign a new value to a function parameter in an ada postcondition
- Postcondition of a method with mypy
- Precondition and postcondition in Java
- How to give the right precondition to prove an assert statemnt in frama-c?
- How can I fix this code with unstoppable loop?
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
Popular # Hahtags
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
No.
In OCL, the construct is
if...then...else...endifso your first example can only be 'equivalent' to a different syntax error.The logical operations are rewritable using
ifconstructs, but considerable care is necessary to ensure that the possibilities with null or invalid inputs do not crash theifcondition term which must be a 2-valuedBoolean.