In dealing with concurrent programs care must be taken when defining the notion of ``correctness''. Traditional sequential programs may be viewed as (partial) functions from inputs to outputs; in such a setting specifications may be given as a pair consisting of a precondition describing the ``allowed'' inputs and a postcondition describing the desired results for these inputs. This notion of specification remains appropriate for a concurrent program representing a ``parallelized'' version of some sequential program; in this case, concurrency (parallelism) has been introduced solely for performance purposes. For reactive, nonterminating and potentially nondeterministic concurrent systems, however, this approach is too limited. This section discusses alternative notions that have been developed and discusses how they have been deployed in reasoning about systems.