search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

[grasshopper] Let procedures / post-condition refer to pre-condition footprint #124

Open septract opened 7 years ago

septract commented 7 years ago

Right now we existentially quantify the footprint separately for the pre/post. We might want to rearrange this so we quantify the pre-footprint in the procedure argument, because this would mean we could compare the pre/post footprint, and refer to it explicitly in procedure calls.

MattWindsor91 commented 7 years ago

Would this at all help with problems relating to assignment? Eg. being able to pure-assume that e is not in the pre-condition footprint. Or is the problem here entirely due to the postcondition?