Programas

Na linguagem SLP um programa P consiste numa lista de declarações seguida de uma instrução de cooperação, na qual os diversos processos que constituem o programa podem ser nomeados:

declarações; [P₁ :: [l₁:S₁; $\widehat{l_1}$:] || $\ldots$ || P_k :: [l_k:S_k; $\widehat{l_k}$:]]

As declarações são uma lista de instruções de declaração da forma:

modo variável, $\ldots$, variável: tipo where $\varphi_i$

Enquanto que nos blocos todas as variáveis declaradas eram locais, nas declarações que começam um programa podem existir os seguintes modos:

• in - qualifica variáveis que são parâmetros de entrada para um programa e que não podem ser modificadas ao longo da sua execução.
• local - qualifica variáveis que são locais a um programa e que não são visíveis fora dele.
• out - qualifica variáveis onde são armazenados resultados de um programa.

Para as variáveis do tipo local e out a asserção $\varphi_i$ serve para inicializar as variáveis e é da forma y=e, apenas podendo a expressão e depender de variáveis in. Para as variáveis de entrada, esta asserção serve para restringir o domínio de valores esperado. A conjunção de todas as asserções que aparecem nas declarações de entrada num programa denomina-se précondição dos dados e define-se como:

$\varphi = \varphi_1 \land \ldots \land \varphi_n$

No SPL é possível especificar instruções de cooperação constituídos por um número parametrizado de processos. Para tal usa-se a seguinte sintaxe:

|| P[j:[1..M]]::S[j]

O mesmo pode ser feito para as instruções de selecção. Neste caso temos:

or P[j:[1..M]]::S[j]