A way of representing the purpose of a function, which upon implementation of the function is elucidated in terms of progressively more specific intended functions. Used in Cleanroom Software Engineering, where analysis is used to "prove" that the method matches the functionality specified by the intended function. See N Notation