The development of types is an important but challenging issue in temporal logic programming. In this paper, we investigate how to formalize and implement types in the temporal logic programming language MSVL, which is an executable subset of projection temporal logic (PTL). Specifically, we extendMSVL with a few groups of types including basic data types, pointer types and struct types. On each type, we specify the domain of values and define some standard operations in terms of logic functions and predicates. Then, it is feasible to formalize statements of type declaration of program variables and statements of struct definitions as logic formulas. As the implementation of the theory, we extend the MSV toolkit with the support of modeling, simulation and verification of typedMSVL programs. Applications to the construction of AVL tree and ordered list show the practicality of the language.
LiuS Y, ChenY T, NagoyaF, McDermid J A. Formal specificationbased inspection for verification of programs. IEEE Transactions on Software Engineering, 2012, 38(5): 1100–1122 https://doi.org/10.1109/TSE.2011.102
2
LeeS U J, DobbieG, SunJ, Groves L. Theorem prover approach to semistructured data design. Formal Methods in System Design, 2010, 37(1): 1–60 https://doi.org/10.1007/s10703-010-0099-4
3
LiuZ Y, PangJ, ZhangC Y. Design and formal verification of a CEM protocol with transparent TTP. Frontiers of Computer Science, 2013, 7(2): 279–297 https://doi.org/10.1007/s11704-013-1268-6
4
DingZ J, JiangC J, ZhouM C. Design, analysis and verification of real-time systems based on time petri net refinement. ACM Transactions on Embedded Computing Systems, 2013, 12(1): 4 https://doi.org/10.1145/2406336.2406340
5
FisherM. An Introduction to Practical Formal Methods Using Temporal Logic. Chichester: John Wiley & Sons, 2011 https://doi.org/10.1002/9781119991472
6
GherghinaC, DavidC, QinS, Chin W N. Expressive program verification via structured specifications. International Journal on Software Tools for Technology Transfer, 2014, 16(4): 363–380 https://doi.org/10.1007/s10009-014-0306-5
PerrinD, PinJ É. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics Series. London, San Diego (Calif.): Academic, 2004
11
DongJ S, LiuY, SunJ, Zhang X. Towards verification of computation orchestration. Formal Aspects of Computing, 2014, 26(4): 729–759 https://doi.org/10.1007/s00165-013-0280-9
DuanZ H, TianC.A unified model checking approach with projection temporal logic. In: Proceedings of the 10th International Conference on Formal Methods and Software Engineering. 2008, 167–186 https://doi.org/10.1007/978-3-540-88194-0_12
14
YangX X, DuanZ H. Operational semantics of framed tempura. The Journal of Logic and Algebraic Programming, 2008, 78(1): 22–51 https://doi.org/10.1016/j.jlap.2008.08.001
ZhangN, DuanZ H, TianC, Du D Z. A formal proof of the deadline driven scheduler in PPTL axiomatic system. Theoretical Computer Science, 2014, 554: 229–253 https://doi.org/10.1016/j.tcs.2013.12.014
17
ZhangP, DuanZ H, TianC. Simulation of CTCS-3 protocol with temporal logic programming. In: Proceedings of the 17th IEEE International Conference on Computer Supported Cooperative Work in Design. 2013, 72–77 https://doi.org/10.1109/cscwd.2013.6580942
18
WangX B, SunT. A method based on MSVL for verification of the social network privacy policy. In: Proceedings of the International Workshop on Structured Object-Oriented Formal Language and Method. 2015, 118–131
TianC, DuanZ H. Expressiveness of propositional projection temporal logic with star. Theoretical Computer Science, 2011, 412(18): 1729–1744 https://doi.org/10.1016/j.tcs.2010.12.047
21
MannaZ, PnueliA. The Temporal Logic of Reactive and Concurrent Systems. New York, NY: Springer-Verlag New York, Inc., 1992 https://doi.org/10.1007/978-1-4612-0931-7
22
LefticaruR, TudoseC, IpateF. Towards automated verification of P systems using Spin. In: de Castro L N, ed. Natural Computing for Simulation and Knowledge Discovery. IGI Global, 2014, 159–170 https://doi.org/10.4018/978-1-4666-4253-9.ch010
WangS L, LongQ, QiuZ Y. Type Safety for FJ and FGJ. In: Proceedings of the International Colloquium on Theoretical Aspects of Computing. 2006, 257–271 https://doi.org/10.1007/11921240_18
25
KeW, LiuZ M, WangS L, Zhao L. A graph-based generic type system for object-oriented programs. Frontiers of Computer Science, 2013, 7(1): 109–134 https://doi.org/10.1007/s11704-012-1307-8
26
CousineauD, Doligez D, LamportL , MerzS, Ricketts D, VanzettoH . Tla+ proofs. In: Proceedings of the International Symposium on Formal Methods. 2012, 147–154 https://doi.org/10.1007/978-3-642-32759-9_14
27
FisherM, HeppleA. Executing logical agent specifications. In: El Fallah Seghrouchni A, Dix J, Dastani M, et al., eds. Multi-Agent Programming: Languages, Tools and Applications. Boston, MA: Springer US, 2009, 1–27 https://doi.org/10.1007/978-0-387-89299-3_1
28
LamportL. The PlusCal algorithm language. In: Proceedings of the International Colloquium on Theoretical Aspects of Computing. 2009, 36–60 https://doi.org/10.1007/978-3-642-03466-4_2
WangX B, DuanZ H, ZhaoL. Formalizing and implementing types in MSVL. In: Proceedings of the 3rd International Workshop on Structured Object-Oriented Formal Language and Method. 2014, 62–75 https://doi.org/10.1007/978-3-319-04915-1_5
31
DuanZ H. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2006
TianC, DuanZ H. Complexity of propositional projection temporal logic with star. Mathematical Structures in Computer Science, 2009, 19(1): 73–100 https://doi.org/10.1017/S096012950800738X
34
KnuthD E. The Art of Computer Programming, Vol 3: Sorting and Searching. 2nd ed. Redwood City, CA: AddisonWesley Longman Publishing Co., Inc., 1998
35
Ben-AriM. Principles of Concurrent and Distributed Programming (Prentice-Hall International Series in Computer Science). 2nd ed. Boston, MA: Addison-Wesley Longman Publishing Co., Inc., 2006
