队列
队列是一种先进先出的数据结构。
    1.取队列中的数据dequeue
    2.向队列中存放数据enqueue
    数据按照先进先出的原则进出队列。
我们有三个数据{p1,p2,p3}，两个操作p_enqueue向队列中存放数据，p_dequeue取队列中数据。

要验证的PPTL性质：
[](p_enqueue.ele=p1 -> <> p_dequeue.res=p1)
含义：在队列中先存放数据p1，那么未来队列中必定先取出p1数据。