[sv-ac] "if else" definition needs corrections - mantis 1786

Yaniv,

the problem that you point has implications to SVA "if else".

"if (b) P1 else P2" is defined in annex E as a shortcut to
"(b |-> P1) and (!b |-> P2)". The problem with this definition
is that b = X, neither P1 nor P2 are required to hold. This is
inconsistent with SV procedural "if else" where the else block
should be executed.


 I enter a mantis item 1786.

A simple correction that will fix that is to define "if (b) P1 else P2"
as a shortcut to "((b ===1) |-> P1) and ((b!==1) |-> P2)".

But with this definition, "if (b) P1 else P2" is not equivalent to
"if (!b) P2 else P1", so I am not sure what do we need.

Doron

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.