Contract an TLAPLUS

Let's take an example.

Suppose an algorithm that takes a graph an returns the nodes of the graph.

So GraphType = SUBSET [ in -> STRING, out -> STRING ]

Nodes(A) == { x \in STRING : \E n \in A : x = n.in \/ x = n.out}

Suppose G is a constant.

And resu a variable.

So the contract of the algorithm is:

Requires == G \in GraphType

Ensures == resu =Nodes(g)

So how can we link formally the contract and the algorithm? This way?

Correctness == Requires /\ Spec => [] ( pc = "Done" => Ensures )