以具量詞之命題時間邏輯及其延伸為表示法的模組化規格與驗證(I)