|
Size: 1159
Comment:
|
Size: 581
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 5: | Line 5: |
| = WikiName Wiki = | = Star Wiki = |
| Line 7: | Line 7: |
| What is this wiki about? | This is a wiki about [[SeparationLogic|separation logic]]. |
| Line 9: | Line 9: |
| Interesting starting points: * RecentChanges: see where people are currently working * WikiSandBox: feel free to change this page and experiment with editing * FindPage: find some content, explore the wiki * HelpOnMoinWikiSyntax: quick access to wiki markup Here is an example how to use the Latex extension installed: <<latex(\usepackage{dsfont} % $$\mathds{C}$$)>> == How to use this site == A Wiki is a collaborative site, anyone can contribute and share: * Edit any page by pressing '''<<GetText(Edit)>>''' at the top or the bottom of the page * Create a link to another page with joined capitalized words (like WikiSandBox) or with {{{[[words in brackets]]}}} * Search for page titles or text within pages using the search box at the top of any page * See HelpForBeginners to get you going, HelpContents for all help pages. To learn more about what a WikiWikiWeb is, read about MoinMoin:WhyWikiWorks and the MoinMoin:WikiNature. This wiki is powered by [[http://moinmo.in/|MoinMoin]]. |
Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system. |
Star Wiki
This is a wiki about separation logic.
Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.