Graph API improvements

[rolyp]

Align graph API with specific operations used by slicing, to avoid extend having a rather weak contract (so that α can always be assumed not to be already in the graph), by introducing separate methods to add edges. Make the operations explicit (new names suggested below) to express the algorithmic goal more directly in the code, and also make bugs less likely (because of the tighter contracts) and expose opportunities for optimisation.

• [x] connectOut and connectIn broken: need to add any newly-added vertex into opposite map
• [x] tighten extend so α is not in graph but αs are
• [x] new “add edge” API
  • [x] connectOut: add edge (α,β) (e.g. during backward slicing), where β may not be in the slice yet but α is
  • [x] connectIn: add edge (α,β) (e.g. during forward slicing), where α may not not be in the slice yet but β is
  • [x] better names for connectOut and connectIn
  • [x] express connectΙn in terms of connectOut and opp
• [x] rename opp to op (by analogy with $C^{\mathsf{op}}$ notation)
• [x] rename extend to add
• [x] relationship between remove and add

[rolyp]

Added provisional spec for the new operations.