M ETODISK TILNÆRMING

dade de mensagens que uma fila possui e definir a capacidade de uma fila de mensagens. Para esse refinamento, características adicionais foram atribuídas ao estado da máquina Queue gerando o refinamento Queue_r. Consequentemente, alterações também foram necessárias às operações refinadas desta máquina. A explicação mais completa de como esse refinamento foi realizado pode ser vista nas seções seguintes.

7.2.1 Estado

A parte do estado do refinamento Queue_r criada para tratar as propriedades de- scritas anteriormente pode ser vista na figura 7.6. Percebe-se que ela é formada essencial- mente por três variáveis queue_size, queue_quant, queue_items_r. A primeira informa o tamanho máximo de mensagens que a fila pode ter. A segunda indica a quantidade de mensagens que a fila tem. Por último, a terceira especifica o conjunto de mensagens de uma fila através da estrutura sequência, na qual cada mensagem tem uma ordem. Um detalhe sobre essas propriedades é que as queue_size e queue_quant foram relacionadas ao conjunto queues e, por isso, essas propriedades foram estendidas para os elementos semáforo e mutex, ao contrário de queue_items_r, que se aplica somente ao elemento fila de mensagens.

REFINEMENT Queue_r INVARIANT . . .

queue_size ∈ QUEUE →+ QUEUE _LENGTH ∧

queue_quant ∈ QUEUE →+ QUEUE _QUANT ∧

queue_items_r ∈ QUEUE →+ iseq(ITEM )∧

dom(queue_size) = queues∧ dom(queue_quant) = queues∧

dom(queue_items_r) = dom(queue_items)∧ . . .

Figura 7.6: Estado do refinamento Queue_r.

A continuação do invariante da máquina Queue_r pode ser vista na figura 7.7. Ele relaciona propriedades já especificadas na máquina Queue às novas criadas no refina- mento em Queue_r. As três primeiras linhas desse invariante informam que a quantidade de itens da nova estrutura de mensagens (sequência) deve ter a mesma quantidade de itens da estrutura anterior (conjunto). Mais a frente é feita uma relação entre o estado de uma fila e a sua quantidade de mensagens. Assim, uma fila de estado cheia deve ter a sua capacidade máxima de mensagens e um fila de estado vazia não deve ter nenhuma men- sagem. Em seguida, a mesma relação é feita ao estado de um semáforo. Por último, é informado que um mutex ocupado deve ter tamanho igual a zero.

7.2.2 Operações

No refinamento Queue_r, as operações foram alteradas para manipular a sequên- cia queue_items_r no lugar do conjunto queue_items e tratar das novas características adicionadas ao estado do refinamento. Assim, ao enviar uma mensagem para uma fila esta mensagem deve ser adiciona na sequência queue_items_r e não mais no conjunto queue_items. Além disso, para cada item enviado ou retirado da fila, o número de men- sagens da fila (queue_quant) deve ser alterado e, caso este fique com o valor zero, a fila deve classificada como fila vazia.

∀(queue).(queue ∈ queues_msg ⇒ ran(queue_items_r (queue)) = queue_items(queue)∧ size(queue_items_r (queue)) = queue_quant(queue))∧

∀(queue).(queue ∈ queues_msg_full ⇒ queue_quant(queue) = queue_size(queue))∧ ∀(queue).(queue ∈ queues_msg ∧ queue_quant(queue) = queue_size(queue)

⇒ queue ∈ queues_msg_full )∧

∀(queue).(queue ∈ queues_msg_empty ⇒ queue_quant(queue) = 0)∧

∀(queue).(queue ∈ queues_msg ∧ queue_quant(queue) = 0 ⇒ queue ∈ queues_msg_empty)∧ ∀(semaphore).(semaphore ∈ semaphores_busy ⇒ queue_quant(semaphore) = 0)∧

∀(semaphore).(semaphore ∈ semaphores ∧ queue_quant(semaphore) = 0 ⇒

semaphore∈ semaphores_busy)∧

∀(semaphore).(semaphore ∈ semaphores_full

⇒ queue_quant(semaphore) = queue_size(semaphore))∧ ∀(semaphore).(semaphore ∈ semaphores ∧ queue_quant(semaphore) = queue_size(semaphore)

⇒ semaphore ∈ semaphores_full )∧ ∀(mutex).(mutex ∈ mutexes ⇒ queue_size(mutex ) = 1)∧

∀(mutex).(mutex ∈ mutexes_busy ⇒ queue_quant(mutex ) = 0)∧

∀(mutex).(mutex ∈ mutexes ∧ queue_quant(mutex ) = 0 ⇒ mutex ∈ mutexes_busy)

Figura 7.7: Continuação do invariante do refinamento Queue_r.

No caso do semáforo, quando este é retido, seu contador (queue_quant) é decremen- tado e, no momento que este é liberado, o seu contador é incrementado. Quando o conta- dor está vazio, o semáforo é dito como ocupado (semaphores_busy) e, quando o contador estiver cheio, o semáforo deve ser classificado como semáforo completamente disponível (semaphores_full). Para o mutex, ocorre o mesmo, só que seu atributo queue_quant sempre será um ou zero. Quando este estiver com o valor zero o semáforo está retido (mutexes_busy), caso contrário ele está disponível.

Para a melhor compreensão, será exibida nesta seção a especificação de uma oper- ação de cada elemento. Desse modo, as operações demonstradas serão: q_sendItem, q_takeSemaphore e q_takeMutex .

7.2.2.1 Refinamento da operação q_sendItem

A parte do refinamento da operação q_sendItem responsável pelas características do módulo Queue_r é mostrada na figura 7.8. Nela, o parâmetro que indica a posição na qual a mensagem será adicionada na fila (copy_position) é verificado inicialmente. Para o valor queueSEND_TO_BACK a mensagem é colocada no final da fila pela substi- tuição queue_items_r(pxQueue) := queue_items_r(pxQueue) ← pxItem e para o outros valores a mensagem é colocoda no início da fila por queue_items_r(pxQueue) := pxItem → queue_items_r (pxQueue). Em seguida, é conferido se, com a nova men- sagem, a fila ficará cheia. Por último, a quantidade de mensagens da fila é incrementada. 7.2.2.2 Refinamento da operação q_takeSemaphore

No refinamento da função q_takeSemaphore, a especificação que está relacionada às características do módulo Queue_r é a exibida na figura 7.9. Nessa modelagem, ini- cialmente decrementa-se o contador do semáforo, informando que este está sendo retido. Caso seu contador esteja cheio, o semáforo é retirado do conjunto de semáforos de con-

q_sendItem(pxQueue, pxItem, copy_position) = BEGIN

IFcopy_position = queueSEND_TO_BACK THEN

queue_items_r(pxQueue) := queue_items_r(pxQueue) ← pxItem ELSE

queue_items_r(pxQueue) := pxItem → queue_items_r(pxQueue)

END�

. . .

IFqueue_quant(pxQueue) + 1 = queue_size(pxQueue) THEN

queues_msg_full := queues_msg_full ∪ {pxQueue}

END�

queue_quant(pxQueue) := queue_quant(pxQueue) + 1 END;

Figura 7.8: Parte do refinamento da operação mathitq_sendItem.

tador cheio, e, caso o semáforo fique com o contador igual a zero, ele é colocado no conjunto de semáforos ocupados.

q_takeSemaphore(semaphore) = BEGIN

queue_quant(semaphore) := queue_quant(semaphore) − 1 �

IFqueue_quant(semaphore) = queue_size(semaphore) THEN

semaphores_full := semaphores_full − {semaphore}

END�

IFqueue_quant(semaphore) − 1 = 0 THEN

semaphores_busy := semaphores_busy ∪ {semaphore}

END�

END;

Figura 7.9: Parte do refinamento da operação mathitq_takeSemaphore.

7.2.2.3 Refinamento da operação q_takeSemaphore

Por último, tem-se o refinamento da operação q_takeSemaphore na figura 7.10. Esse refinamento é bastante simples e se diferencia da operação abstrata da figura 6.23 somente pelo fato de que a característica queue_quant é incrementada no momento que o mutex é retido.

q_takeMutex (mutex , task) = BEGIN

queue_quant(mutex ) := queue_quant(mutex ) − 1 � mutexes_busy := mutexes_busy ∪ {mutex } � mutex_holder(mutex ) := task

END;