Home » forums » LtU Forum

Abstraction wins: An approach to framing and mutability

Tony Hoare wrote his paper "An axiomatic basis for computer programming" in 1969. This led to the so called "Hoare Logic" for software verification.

Up to now all attempts to prove software correct which is written in a language which allows mutable types and references have not yet been satisfactory because of the "framing" or "alias" problem. An object might be reached through different references. Therefore it is necessary to specify not only what a procedure modifies, but also what it leaves unchanged.

Various techniques have been invented to get a hand on this problem: Separation logic, alias calculus, "modify/use" annotations.

In the paper An approach to framing and mutability a new approach is described. It is based on implicit frame contracts. The writer of a procedure just specifies what the procedure is going to modify with the implicit contract that it modifies nothing unspecified. By using a dependency graph of all functions a complete frame contract can be derived from the implicit frame contract.

The paper demonstrates that the derived frame contracts coincide with the ones a user is expecting intuitively.

By hbrandl at 2012-06-03 19:32 | LtU Forum | previous forum topic | next forum topic | other blogs | 4412 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

framing the world

Very interesting, thank you for the paper.

What about framing the 'world' itself, in the sense of what can (be) change(d), in general as opposed to the context of a single procedure? Everything else is not part of the world, thus either it cannot change or its changing does not influence the program semantics (eg output ports).

Denis

By spir at Wed, 2012-06-06 23:15 | login or register to post comments

Could you elaborate more on

Could you elaborate more on what you mean by "framing the world".

If you talk about output ports you probably are in the context of concurrency.

By hbrandl at Wed, 2012-06-06 23:24 | login or register to post comments

I am struggling to understand the rules added

I am struggling to understand the rules added by the verifier.

Why does a procedure which takes an argument b: CURRENT need rules like:

all (a: CURRENT)
require
  a /~ b
ensure
  a.count = old a.count
end

Can the procedure affect other variables of the current type? And if it can, why is there no rule for all (x: String), all (y: Numeral) etc?

By Denis Bredelet -jido at Tue, 2012-06-12 07:10 | login or register to post comments

Replying to myself: read

Replying to myself: read again from the top, it is all about identity/equality rules with regards to mutable types.

I will meditate on it.

By Denis Bredelet -jido at Tue, 2012-06-12 07:57 | login or register to post comments

It is all about framing

@Denis

It has to be clear from the user's point of view what a routine changes and what it leaves unmodified. In theory all other types have to be added as well "all(x:STRING) ..., all(y:NUMERAL)...". But these are already different types. And strings and numerals are immutable anyhow.

We need framing conditions for all mutable objects which might be reached by one of the arguments of the procedure.

By hbrandl at Tue, 2012-06-12 16:53 | login or register to post comments

How?

We need framing conditions for all mutable objects which might be reached by one of the arguments of the procedure.

Precisely. So, how can a:CURRENT with a /~ b be reached by the procedure?

By Denis Bredelet -jido at Tue, 2012-06-12 21:05 | login or register to post comments

derivable conditions

Hi Denis,

your common sense is absolutely right. But we need to derive the conditions formally, i.e. a machine has to be able to derive these conditions. The framing conditions from a user's point of view must be derivable by looking at the contract only. The user does not know whether the object has some internal references to other objects of the same type.

Let us take the example of "extend_rear". The contract looks like

   extend_rear(b:CURRENT, e:G)
       require
           not b.is_full
       ensure
           -- explicit contract
           b.content = old (b.content + e)
           -- derived frame contract
           all(a:CURRENT) a/~b => a.content = old a.content
       end

This contract says that the procedure "extend_rear" modifies the function "content". But it modifies the function only at "b". And the contract says as well that "extend_rear" does not modify any other visible function.

We can regard a function as some global variable. The procedure "extend_rear" assigns to the function "content" a new value. The new value of the function is the same as the old one except at one argument position.

The user of the procedure "extend_rear" might need this information for his own reasoning. Look at the following code snippet:

  local
       a,b:BUFFER[CHARACTER]
  do
       ...
       check
           no_alias: a /~ b
           a.content = x
           b.content = y
       end
       a.extend_rear('a')
       check
           a.content = x + 'a'
           b.content = y
       end
       ...
  end

The verifier can verify this code snippet only if the condition "no_alias" is available (or derivable from some other information) and if it can derive the complete frame contract of "extend_rear".

I.e. the verifier does exactly the same as your common sense is telling you.

But the situation is not always that trivial. Consider a self referential structure (a single or doubly linked list, a tree or a general graph). The formal derivation of the frame contracts does work in this complicated setting as well. Note that in these cases it is far from trivial what objects might be reached from one object. Changing a reference of one linkable object changes each structure which can reference the linkable element (other lists, trees, graphs, iterators, ... )

By hbrandl at Wed, 2012-06-13 03:58 | login or register to post comments