Mathematics of indirect assignment (C-pointers)

[stephengaito]

Yet again many thanks for an excellent tutorial.

Alas, I have fallen into my "Mathematician of very little brain" mode.... I am having trouble understanding the mathematics which underlies your discussion in section 4.1.1.1 "Assignment of pointed value".

At the height of 10,000 meters, I can follow your discussion (after a couple of re-readings).

However I am finding it difficult to find, what is for me, a Mathematically rigorous interpretation of your discussion. For me, at the moment, I think you are mixing syntax and semantics, which for me should be kept as distinct parts of your discussion.

The rest of the chapter (which I have skimmed) is fairly standard and I know of other expositions which give pretty much the same mathematical meaning/exposition.

As we both know, there are very few, if any, expositions which deal directly with indirect assignment (C-pointers).

Where can I find a rigorous discussion of the "weakest precondition predicate" for indirect assignment (C-pointers)?

Which discussions/papers are you or your team using?

[AllanBlanchard]

However I am finding it difficult to find, what is for me, a Mathematically rigorous interpretation of your discussion. For me, at the moment, I think you are mixing syntax and semantics, which for me should be kept as distinct parts of your discussion

I'd be happy to fix this, the formal part is always the one that is the harder for me to write by hand (reason why I am less worried when I am writing things directly in Why3 for example). So if you can point out exactly which sections mix things that should not, that would be great.

After reading it again, maybe what's not clear is that the memory is viewed as a function, but I would not bet.

Where can I find a rigorous discussion of the "weakest precondition predicate" for indirect assignment (C-pointers)?

The WP model is inspired from Burstall (Some Techniques for Proving Correctness of Programs which Alter Data Structures), unfortunately, I cannot find the paper :( . I have to admit that I never dived into the details of how WP came to this modeling of the memory (since it was already there long before I joined the development).

[stephengaito]

It may be that I, in my "Mathematician of very little brain" mode, am just being a pedant :-)

From my understanding of Denotational/Operational Semantics, I was expecting the "memory as a function" and yes I can see it... I think my problem may be that your notation, for me, clouds various concepts I feel need to be kept very separate.

I have ordered the conference proceedings in which Burstall's paper was published from Warwick University Library's internal store... it should be ready for me to pick up on Tuesday.

I think that really the best way for me to communicate what is bothering me is to actually develop the Mathematical theory myself from "first principles" and then post my rendition as AMS-LaTeX in this issue. I think that by using AMS-LaTeX you should be able to cut and paste any relevant bits into your tutorial should you want to.

This may take me a week or so, I suspect I will have a couple of drafts to post as I explore what I think this all should mean.

[AllanBlanchard]

I have ordered the conference proceedings in which Burstall's paper was published from Warwick University Library's internal store... it should be ready for me to pick up on Tuesday.

Maybe two remarks:

• WP does not exactly implement this model, IIRC it is less sophisticated on some aspects (separation of structure fields for examples), and also does some optimization to avoid modeling memory with a function when possible,
• WP also optimizes the generation of VCs following Leino's style (Leino. Efficient weakest preconditions), but does not entirely implement this methods, it behaves slightly differently on conditional statements for example.

So the explanation in the tutorial is not meant to be exactly what happens in WP (in particular, I didn't try to add this in the tutorial because I prefer to wait for the new memory model).

This may take me a week or so, I suspect I will have a couple of drafts to post as I explore what I think this all should mean.

Thank you!

[stephengaito]

Getting Burstall's paper is more for historical completeness, I suspect I will ignore it until I am done and then see how close or far I am from his thinking.

I suspect my rendition will be rather far from how it works practically in Frama-C, which I ok as far as I am concerned. It will need to be made more practical in stages.