5
$\begingroup$

My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the type of the result of the computation and Pre and Post are propositions representing respectively the pre and postconditions of the statement and res is the result of type T which can appear in the postcondition.

Given the following program in pseudo-C:

int i=0;
int*p=&i;
*p=1
return i;

How can Hoare type theory represent the the fact that i must be 1?After all,it's not clear i is modified in the above snippet,and it can be hidden even from the programmer if we begin to add lambdas and partial application

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ I'm new to Hoare Logic myself, but I would imagine you should attempt to show {Pre}res:T{Post} is valid modulo the Theory of Pointers. For which, you should find or define the Theory of Pointers. Similar to how a[i] = 1; j = i; a[j] = 2 should result in a[i] = 2. A Hoare triple for this would be provable modulo the Theory of Arrays. $\endgroup$
    – ryan
    Oct 2, 2017 at 17:21
  • $\begingroup$ The problem is combining with closures,for example:i:var int=0;f=()->{i++};/*some other code...*/;f() In this case the runtime is creating a funpointer+pointer to &i,without taking the explicit address of i $\endgroup$
    – Pasqui23
    Oct 2, 2017 at 21:23

1 Answer 1

Reset to default
8
$\begingroup$

A pointer to a variable creates an alias. When the alias is modified, the corresponding variable is modified as well. Therefore, the rule for an assignment in Hoare's logic is not just update the value, but update the value for all associated aliases. Let's apply it to the example:

{True}        int i=0;  {i = 0}
{i = 0}       int*p=&i; {i = 0; [*p, i]}  /* *p and i are now aliases */
                                          /* The postcondition can be written as: */
                        {[*p, i] = 0}     /* In particular, *p = 0 */
{[*p, i] = 0} *p=1;     {[*p, i] = 1}     /* In particular, i = 1 */
{[*p, i] = 1} return i; {i = 1}

The general rules to reason about programs with pointers are given by Separation logic. The information whether two expressions reference the same memory location is obtained by pointer analysis and alias analysis.

Improve this answer
$\endgroup$
2
  • $\begingroup$ So Hoare types includes Separation logic and alias analysis? $\endgroup$
    – Pasqui23
    Oct 3, 2017 at 10:10
  • 2
    $\begingroup$ Hoare logic is a framework that can be used in different applications areas. Separation logic is an extension of Hoare logic with some new operators relying on disjoint memory locations. Pointer and alias analyses can be used to check whether the memory locations are disjoint indeed. $\endgroup$
    – Alexander Kogtenkov
    Oct 3, 2017 at 14:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.