I have the following def's
Sns : Stm → (State ֒→ State)
Sns[S] = s' (if <S,s> -> s') else undefined
I'm wondering if Sns is a partial or total function. I think it's total since it always returns a partial function, given any statement.
But the book I'm reading (semantic with application by wiley, pg 41) says:
Note that Sns is a well-defined partial function because of Theorem 2.9. The need for partiality is demonstrated by the statement
while true do skipthat always loops.
I'm very confused.