+
Skip to content

Conversation

nomeata
Copy link

@nomeata nomeata commented Apr 13, 2023

This transformation make explicit the following implicit side conditions
of terms in premises and conclusions:

  • Array access a[i] i < |a|
  • Joint iteration e*{v1,v2} |v1*| = |v2*|
  • Option projection !(e) e =!= null

Depends upon #6 and #5.

nomeata added 3 commits April 8, 2023 21:56
This transformation make explicit the following implicit side conditions
of terms in premises and conclusions:

 * Array access          a[i]         i < |a|
 * Joint iteration       e*{v1,v2}    |v1*| = |v2*|
 * Option projection     !(e)         e =!= null

Depends upon #6 and #5.
f52985 added a commit that referenced this pull request Apr 21, 2023
This transformation will
1) make the equality conditions explicit as assignment conditions, if they are indeed assignments, and
2) reorder the premises that resembles the actual order of execution in interpreter

Depends upon #9.
@f52985 f52985 mentioned this pull request Apr 21, 2023
@f52985 f52985 merged commit 37d4ca0 into main Apr 24, 2023
@nomeata nomeata deleted the sideconditions branch April 24, 2023 08:45
Alan-Liang pushed a commit to Alan-Liang/spectec that referenced this pull request Sep 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

点击 这是indexloc提供的php浏览器服务,不要输入任何密码和下载