Frame problem: Difference between revisions
Jump to navigation
Jump to search
imported>The Anome →Fluent calculus solution: fmt source |
imported>Missmodal Link suggestions feature: 1 link added. |
||
| Line 172: | Line 172: | ||
captures that code which sorts a list ''x'' does not unsort a separate list ''y,'' and it does this without mentioning ''y'' at all in the initial spec above the line. | captures that code which sorts a list ''x'' does not unsort a separate list ''y,'' and it does this without mentioning ''y'' at all in the initial spec above the line. | ||
Automation of the frame rule has led to significant increases in the scalability of automated reasoning techniques for code,<ref>{{Cite journal|last1=Calcagno Cristiano|last2=Dino Distefano|last3=Peter O'Hearn|last4=Hongseok Yang|date=2011-12-01|title=Compositional Shape Analysis by Means of Bi-Abduction|journal=[[Journal of the ACM]]|language=EN|volume=58|issue=6|pages=1–66|doi=10.1145/2049697.2049700|s2cid=52808268|url=https://ora.ox.ac.uk/objects/uuid:bcfefe74-a79c-4155-8160-c51f92f05466}}</ref> eventually deployed industrially to codebases with tens of millions of lines.<ref>{{Cite journal|first1=Dino |last1=Distefano|first2=Manuel |last2=Fähndrich|first3=Francesco |last3=Logozzo|first4=Peter |last4=O'Hearn|date=2019-07-24|title=Scaling static analyses at Facebook|journal=Communications of the ACM|language=EN|volume=62|issue=8|pages=62–70|doi=10.1145/3338112|doi-access=free}}</ref> | Automation of the frame rule has led to significant increases in the scalability of [[automated reasoning]] techniques for code,<ref>{{Cite journal|last1=Calcagno Cristiano|last2=Dino Distefano|last3=Peter O'Hearn|last4=Hongseok Yang|date=2011-12-01|title=Compositional Shape Analysis by Means of Bi-Abduction|journal=[[Journal of the ACM]]|language=EN|volume=58|issue=6|pages=1–66|doi=10.1145/2049697.2049700|s2cid=52808268|url=https://ora.ox.ac.uk/objects/uuid:bcfefe74-a79c-4155-8160-c51f92f05466}}</ref> eventually deployed industrially to codebases with tens of millions of lines.<ref>{{Cite journal|first1=Dino |last1=Distefano|first2=Manuel |last2=Fähndrich|first3=Francesco |last3=Logozzo|first4=Peter |last4=O'Hearn|date=2019-07-24|title=Scaling static analyses at Facebook|journal=Communications of the ACM|language=EN|volume=62|issue=8|pages=62–70|doi=10.1145/3338112|doi-access=free}}</ref> | ||
There appears to be some similarity between the separation logic solution to the frame problem and that of the fluent calculus mentioned above.{{explain|date=May 2022}} | There appears to be some similarity between the separation logic solution to the frame problem and that of the fluent calculus mentioned above.{{explain|date=May 2022}} | ||