Add rand example to Semantics of K document #406
Conversation
xc93
changed the title
| and \prule{Axiom D} is needed in there. | ||
|
|
||
|
|
||
|
|
There was a problem hiding this comment.
Instead of the below, which is essentially the same as you have already written in more details above, could you put a link to the #kore conversation? I'm not sure whether that is accessible by all, but if it's in a comment, it won't be printed and still be accessible by us.
There was a problem hiding this comment.
You mean adding a link of this document to #kore, adding the link to #kore discussion to the document?
|
@Hreada Would it be too much to ask for a PR adding to the semantics of K translations of K rules and all-path/one-path reachability rules with requires/ensures to KORE? |
docs/semantics-of-k.tex
Outdated
| of ``one-path next'' $\snext$, called ``all-path next''. | ||
| The axiom says that \emph{for all next states} of $\rand$, | ||
| it must be some positive number. | ||
| \prule{Axiom A} and \prule{Axiom D} captures the intended semantics |
There was a problem hiding this comment.
Did you mean to include "Axiom A" here? The reminder of the sentence seems to imply a single axiom (e.g. "captures" instead of "capture")
There was a problem hiding this comment.
That's a typo. Thanks for pointing out. It should be "capture".
@traiansf One-path RL is fully covered in a tech report that Grigore and I have finished. I can add what we have agreed on about ensure/requires to the document, but maybe in another PR. This PR also contains an important fix that removes some strange UTF-8 chars to make the TeX file compilable, so I want this PR to merge asap. |
|
I've reopened this as #414 |
Closes #406 * Make result indeterminate when trying to bind an already bound variable with a different expression. This was returning a failing result before, causing a soundness bug, because in some cases rules with duplicate variables in LHS would not be applied. * Make result indeterminate when unifying an injection with a variable. This allows us to get a clear remainder instead of a weird swapped substitution item * Only report violating substitution items
Closes #406 * Make result indeterminate when trying to bind an already bound variable with a different expression. This was returning a failing result before, causing a soundness bug, because in some cases rules with duplicate variables in LHS would not be applied. * Make result indeterminate when unifying an injection with a variable. This allows us to get a clear remainder instead of a weird swapped substitution item * Only report violating substitution items
Closes #406 * Make result indeterminate when trying to bind an already bound variable with a different expression. This was returning a failing result before, causing a soundness bug, because in some cases rules with duplicate variables in LHS would not be applied. * Make result indeterminate when unifying an injection with a variable. This allows us to get a clear remainder instead of a weird swapped substitution item * Only report violating substitution items
The rand example in Section 4.5 illustrates how to correctly define the semantics of
randusing matching logic axioms.Related Slack message:
https://runtimeverification.slack.com/archives/CC360GUTG/p1546707583193800
Reviewer checklist
stack test --coveragestack haddockstylish-haskell