jstolarek / slicer

Companion code for paper "Imperative Functional Programs that Explain their Work", Wilmer Ricciotti, Jan Stolarek, Roly Perera and James Cheney, ICFP 2017, Oxford, UK
http://dl.acm.org/citation.cfm?id=3110258
GNU General Public License v3.0
7 stars 0 forks source link

Need help: Store handling during slicing #67

Closed jstolarek closed 7 years ago

jstolarek commented 7 years ago

In the current implementation backward slicing is carried out in an empty store. I'm not sure if that's correct. Shouldn't we begin backward slicing in a store saved after tracing?

I'm also not sure about initial store and environment for forward slicing. I believe the initial environment for forward slicing should be a final environment produced by backward slicing. And the initial store should be a store saved before tracing. Does that sound right?

jamescheney commented 7 years ago

In backward slicing, the store argument indicates what part of the store we "care about". We don't currently have a primitive for slicing with respect to the value of a label in the store (as opposed to the result of the computation), so this is empty. We should not use the full store saved after tracing for this unless we want an explanation of everything in the store.

For forward slicing, the initial environment should be a prefix of the original initial environment, which could for example be the final environment recovered by backward slicing (but doesn't have to be). The initial store should be a prefix of the original initial store, again this could be one recovered by backward slicing but doesn't have to be.

jstolarek commented 7 years ago

Thanks!