In order to describe the real-time behaviours of programs in terms of
Duration Calculus, proposed by Zhou Chaochen, C.A.R. Hoare
and A.P. Ravn in [4], which can
specify real-time requirements of computing systems,
quantifications over program variables are inevitable,
e.g. to describe local variable declaration, to declare
internal channel
and so on. So a higher-order duration
calculus (abbreviated HDC) is established
in [2]. This paper proves completeness of
HDC on abstract domains by encoding HDC into a complete first-order
two-sorted interval temporal logic. This idea is hinted by
[10]. All results shown in this paper are done under
the assumption that all program variables have finite
variability.
