+++
title = "Detailed implementation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g2"]
forwardlinks = ["3a8g2b"]
zettelid = "3a8g2a"
+++

Destruction of GSA is actually quite tricky to do correctly, as a lot of
information was lost during it's construction, and there are currently
not enough strong well-formedness conditions about the predicates in the
γ and η functions. Especially the γ functions need to be turned into φ
functions, which essentially means reconstructing control-flow
information just from the predicates.

These predicates should be correct, which is hard to quantify itself,
and actually does not relate to the control-flow in any way without
having additional restrictions. The only thing one knows for certain is
that the semantics ensure that the program will not block, meaning there
will always be a predicate that is true, which allows the semantics to
advance. This does not help for the destruction though, as this does not
guarantee that the predicates talk about the control-flow paths in any
way. For that one will have to add a well-formedness condition
specifically for the destruction which will be true when the predicates
do relate to control-flow in some way.