No it isn't. You just need to formally specify what you want to happen, then reason as to whether this leads to adequate semantics for the component being buil

No it isn't. You just need to formally specify what you want to happen, then reason as to whether this leads to adequate semantics for the component being built, and iterate until satisfactory semantics are achieved. This just happens to be the definition of programming.