[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Help with choose (pvs dump file)




Oops, got a little carried away in emacs and sent the previous
message before attaching the dump file.

Here it is.


%Patch files loaded: patch2 version 2.417

$$$Test.pvs
Test : THEORY

BEGIN

%
% Address of nodes in the network
%
Address : TYPE = { server, client }

%
% Packet Datatype
%   src - Source address of packet
%   dest - Destination of packet
%
Packet : TYPE = [#
  src : Address,
  dest : Address
#]

%
% Node Datatype
%
%  addr - Address of Node
%  outQ - Queue of packets generated by a node
%
IMPORTING Queue[Packet]

Node : TYPE = [#
  addr : Address,
  outQ : Queue[Packet]
#]

%
% A new node has an empty output queue and the specified
% node address
%
newNode(a : Address) : Node = (# 
  addr := a,
  outQ := empty[Packet]
#)

%
% A Network is a set of nodes
%
Network : TYPE = setof[Node]

%
% A new network is a set of new nodes
%
newNetwork : Network = 
  { n : Node | n = newNode(addr(n)) }

net : VAR Network
node : VAR Node
n1, n2 : VAR Node
pkt : VAR Packet
q : VAR Queue[Packet]
a : VAR Address

%
% The next state of a node defines how a node 
% changes when it receives a packet.
%
% If the packet is addressed to the node, then the
% node generates a new packet with the source and 
% destination address of the original packet swapped
%
nextState(pkt : Packet, node : Node) : Node = 
  IF addr(node) = dest(pkt) THEN
    node WITH [ 
      outQ := enqueue(
        pkt WITH [ 
          src := dest(pkt),
          dest := src(pkt)
        ], outQ(node))
    ]
  ELSE 
    node
  ENDIF

%
% The next state of a network is the set of nodes 
% after each node has processed the specified packet.
%
nextState(pkt : Packet, net : Network) : Network = 
  image( (LAMBDA (n: Node): nextState(pkt, n)), net)

%
% Choose a node from a nonempty network.  If there is a 
% node in the network with a nonempty output queue, then
% choose one of those nodes.  Otherwise choose an arbitrary
% node.
%
chooseNode(net : (nonempty?[Node])) : Node =
  LET pktNodes = filter(net, (LAMBDA (n:Node): nonempty?(outQ(n)))) IN
  IF nonempty?(pktNodes) THEN
    choose(pktNodes)
  ELSE
    choose(net)
  ENDIF
 
%
% Prove that every node that receives a packet addressed to it
% will generate a new packet in its output queue.
%
every_node_outputs : THEOREM
  dest(pkt) = addr(node)
  IMPLIES
  nonempty?(outQ(nextState(pkt, node)))
 
%
% Prove that every network that contains a node with the destination
% address of a packet will contain a node with a nonempty output queue
% after the packet is processed by the network.
%
every_network_outputs : THEOREM
  member(node, net) AND
  dest(pkt) = addr(node)
  IMPLIES
  EXISTS (n: Node): member(n, nextState(pkt, net)) AND 
    nonempty?(outQ(n))

%
% Prove that from every network that contains a node with the destination
% address of a packet, a node can be chosen which has a nonempty
% output queue.
%
chosen_node_outputs : THEOREM
  member(node, net) AND 
  dest(pkt) = addr(node)
  IMPLIES
  nonempty?(outQ(chooseNode(nextState(pkt, net))))


END Test

$$$Test.prf
(|Test| (|every_node_outputs| "" (GRIND) NIL)
 (|every_network_outputs| "" (SKOSIMP)
  (("" (INST 1 "nextState(pkt!1, node!1)") (("" (GRIND) NIL)))))
 (|chosen_node_outputs_TCC1| "" (SKOSIMP)
  (("" (EXPAND "nextState")
    (("" (LEMMA "nonempty_member[Node]")
      (("" (INST?)
        (("" (ASSERT)
          (("" (INST 1 "nextState(pkt!1, node!1)")
            (("" (LEMMA "nonempty_member[Node]")
              ((""
                (INST -1
                 "image((LAMBDA (n: Node): nextState(pkt!1, n)), net!1)")
                (("" (ASSERT) (("" (GRIND) NIL)))))))))))))))))))
 (|chosen_node_outputs| "" (SKOSIMP)
  (("" (EXPAND "nextState")
    (("" (EXPAND "image")
      (("" (EXPAND "nextState")
        (("" (EXPAND "chooseNode")
          (("" (GROUND)
            (("1" (HIDE 1)
              (("1" (EXPAND "filter")
                (("1" (ASSERT) (("1" (POSTPONE) NIL)))))))
             ("2" (POSTPONE) NIL))))))))))))))

$$$Queue.pvs
Queue [T: TYPE+] : THEORY
  BEGIN

  Queue : TYPE+

  q, q1, q2: VAR Queue

  empty?, nonempty?: [Queue -> boolean]
  
  queue_disjoint: AXIOM NOT empty?(q) IFF nonempty?(q)
  
  queue_inclusive: AXIOM empty?(q) OR nonempty?(q)
  
  exists_nonempty: AXIOM (EXISTS (x: [[T, Queue] ->(nonempty?)]):TRUE)

  exists_empty: AXIOM (EXISTS (x: [[T, Queue] ->(empty?)]):TRUE)

  enqueue: [T, Queue -> (nonempty?)]
  
  first: [(nonempty?) -> T]

  last: [(nonempty?) -> T]  

  dequeue: [(nonempty?) -> Queue]

  length: [Queue -> nat]
  
  empty: (empty?)
  
  e: VAR T
  
  e1, e2: VAR T
  
  nq, nq1, nq2: VAR (nonempty?)
  
  empty1, empty2: VAR (empty?)
  
  empty_extensionality: AXIOM empty1 = empty2
  
  enqueue_extensionality: AXIOM
        first(nq1) = first(nq2) AND dequeue(nq1) = dequeue(nq2) IMPLIES nq1 = nq2
  
  enqueue_eta: AXIOM enqueue(first(nq), dequeue(nq)) = nq

  first_enqueue: AXIOM
        first(enqueue(e, q)) = 
        IF empty?(q) THEN e
        ELSE first(q)
	ENDIF
  
  dequeue_enqueue: AXIOM
        dequeue(enqueue(e, q)) = 
 	IF empty?(q) THEN q
        ELSE enqueue(e, dequeue(q))
	ENDIF

  last_enqueue : AXIOM
        last(enqueue(e, q)) = e

  p: VAR pred[Queue]
  
  queue_induction: AXIOM
        ((FORALL (q: Queue): empty?(q) IMPLIES p(q))
             AND (FORALL (e: T), (q1: Queue): p(q1) IMPLIES p(enqueue(e, q1))))
            IMPLIES (FORALL (q2: Queue): p(q2))
  
  length_dequeue: AXIOM length(dequeue(nq)) = length(nq) - 1
  
  length_enqueue: AXIOM length(enqueue(e, q)) = length(q) + 1

  length_empty: AXIOM empty?(q) IFF length(q) = 0
  
  empty_is_not_nonempty: LEMMA NOT empty?(q) IMPLIES nonempty?(q)
  
  nonempty_is_not_empty: LEMMA NOT nonempty?(q) IMPLIES empty?(q)
  
  nonempty_enqueue: LEMMA NOT empty?(enqueue(e, q))

  empty_is_empty?: LEMMA empty?(q) IFF q = empty

  member(e: T, q: Queue) : RECURSIVE bool = 
    IF q = empty THEN
      false
    ELSIF first(q) = e THEN
      true
    ELSE
      member(e, dequeue(q))
    ENDIF
    MEASURE length(q) 

  member_enqueue: LEMMA
    member(e1,q) IMPLIES member(e1, enqueue(e2,q))

  member_enqueue1: LEMMA
    member(e, enqueue(e,q))

  END Queue



$$$Queue.prf
(|Queue|
 (|enqueue_TCC1| "" (LEMMA "exists_nonempty") (("" (PROPAX) NIL)))
 (|empty_TCC1| "" (LEMMA "exists_empty") (("" (ASSERT) NIL)))
 (|first_enqueue_TCC1| "" (SKOSIMP)
  (("" (LEMMA "queue_disjoint")
    (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL)))))))))
 (|nonempty_enqueue| "" (GRIND) NIL)
 (|empty_is_empty?| "" (LEMMA "empty_extensionality")
  (("" (GRIND) NIL)))
 (|member_enqueue| "" (SKOSIMP)
  (("" (EXPAND "member")
    (("" (GROUND)
      (("1" (LEMMA "nonempty_enqueue")
        (("1" (INST?) (("1" (ASSERT) NIL)))))
       ("2" (LEMMA "first_enqueue")
        (("2" (INST?)
          (("2" (REPLACE -1 1)
            (("2" (HIDE -1)
              (("2" (LIFT-IF)
                (("2" (LEMMA "empty_is_empty?")
                  (("2" (INST -1 "q!1")
                    (("2" (REPLACE 4 -1)
                      (("2" (ASSERT) NIL)))))))))))))))))
       ("3" (LEMMA "nonempty_enqueue")
        (("3" (INST?) (("3" (ASSERT) NIL)))))
       ("4" (LEMMA "empty_is_empty?")
        (("4" (INST -1 "q!1")
          (("4" (ASSERT)
            (("4" (EXPAND "member" 3)
              (("4" (GROUND)
                (("1" (LEMMA "dequeue_enqueue")
                  (("1" (INST?)
                    (("1" (ASSERT)
                      (("1" (REPLACE -1 -2)
                        (("1" (LEMMA "nonempty_enqueue")
                          (("1" (INST -1 "e2!1" "dequeue(q!1)")
                            (("1" (ASSERT) NIL)
                             ("2" (LEMMA "queue_disjoint")
                              (("2"
                                (INST?)
                                (("2" (ASSERT) NIL)))))))))))))))))
                 ("2" (EXPAND "member" -1)
                  (("2" (GROUND)
                    (("1" (LEMMA "dequeue_enqueue")
                      (("1" (INST -1 "e2!1" "q!1")
                        (("1" (REPLACE -1 2)
                          (("1" (HIDE -1)
                            (("1" (ASSERT)
                              (("1"
                                (LEMMA "first_enqueue")
                                (("1"
                                  (INST -1 "e2!1" "dequeue(q!1)")
                                  (("1"
                                    (REPLACE -1 2)
                                    (("1"
                                      (HIDE -1)
                                      (("1"
                                        (LEMMA "empty_is_empty?")
                                        (("1"
                                          (INST -1 "dequeue(q!1)")
                                          (("1" (ASSERT) NIL)
                                           ("2"
                                            (LEMMA "queue_disjoint")
                                            (("2"
                                              (INST -1 "q!1")
                                              (("2"
                                                (ASSERT)
                                                NIL)))))))))))))
                                   ("2"
                                    (LEMMA "queue_disjoint")
                                    (("2"
                                      (INST -1 "q!1")
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))
                     ("2" (POSTPONE) NIL)))))))))))))))))))))
 (|member_enqueue1| "" (SKOSIMP)
  (("" (EXPAND "member")
    (("" (GROUND)
      (("1" (LEMMA "nonempty_enqueue")
        (("1" (INST?) (("1" (ASSERT) NIL)))))
       ("2" (HIDE 3)
        (("2" (LEMMA "dequeue_enqueue")
          (("2" (INST?)
            (("2" (REPLACE -1 2)
              (("2" (HIDE -1)
                (("2" (LIFT-IF)
                  (("2" (GROUND)
                    (("1" (LEMMA "first_enqueue")
                      (("1" (INST?) (("1" (ASSERT) NIL)))))
                     ("2" (EXPAND "member")
                      (("2" (LEMMA "nonempty_enqueue")
                        (("2" (INST?)
                          (("1" (ASSERT)
                            (("1" (GROUND) (("1" (POSTPONE) NIL)))))
                           ("2" (POSTPONE)
                            NIL))))))))))))))))))))))))))))