The definition of weakest precondition for a non-deterministic language

Question

In the classical IMP language, the definition of weakest precondition is:

definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t"

This is stating that from state s, after executing c we get to a state satisfying Q. My question comes when handling the IF FI construct in the language of guarded commands (see selection command in Wikipedia). My guess is that in this case one needs to define:

definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ (∀ t'. (c,s) ⇒ t' ⟶ Q t')"

I wonder if this is correct and whether it is the standard way of writing it in the literature.

Currently, I'm having problems proving the weakest precondition definition for the sequential composition of commands:

"wp (c1;;c2) Q s = wp c1 (wp c2 Q) s" 

So, I'm beginning to think my definition is wrong. Quoting wikipedia:

the result of this function, denoted wp(S,R), is the "weakest" precondition on the initial state ensuring that execution of S terminates in a final state satisfying R.

so termination is required in the definition, and this is not properly imposed so far. There could be non-terminating branches.