for, while)string
Todos os operadores (exceto os com símbolos, como +) podem ser aplicados de duas formas em Quint:
operador(arg0, ..., argn)arg0.operador(arg1, ..., argn)
Escolha a forma que você acha mais fácil de ler!
Conjuntos, ou Sets, são a principal estrutura de dados em Quint em TLA+.
O tipo de um conjunto é dado por Set[<elemento>]. Ou seja, um conjunto de inteiros tem tipo Set[int].
Criando conjuntos:
Set(1, 2, 3) // Set(1, 2, 3) 1.to(3) // Set(1, 2, 3)
Em linguagens funcionais, usamos muito a função map, que permite a aplicação de uma função a cada elemento de um conjunto.
Set(1, 2, 3).map(x => x * 2) // Set(2, 4, 6)
Pode ser usado com lambdas (operadores anônimos), como acima, ou com operadores nomeados:
pure def quadrado(x: int): int = x * x Set(1, 2, 3).map(quadrado) // Set(1, 4, 9)
Dado um conjunto de duplas, podemos aplicar um operador em cada uma das duplas. Mas cuidado! Se o operador espera dois argumentos, temos que fazer o unpacking das duplas, utilizando parênteses duplos.
pure def soma(x: int, y: int): int = x + y Set((1, 1), (2, 3)).map(soma) // static analysis error: error: [QNT000] Expected 1 arguments, got 2 Set((1, 1), (2, 3)).map(((a, b)) => soma(a, b)) // Set(2, 5)
pure def somaDupla(t: (int, int)): int = t._1 + t._2 Set((1, 1), (2, 3)).map(somaDupla) // Set(2, 5)
O map só nos ajuda quando queremos um conjunto como retorno.
map não pode ser usado para as seguintes operações:
Lembram quais funções podem ajudar com esses casos?
Exemplo: Dado um conjunto de números, retorne um conjunto apenas com os números pares.
Set(1, 2, 3, 4).filter(x => x % 2 == 0) // Set(2, 4)
Argumentos do fold
Exemplo: Dado um conjunto de números, retorne a soma de todos esses números.
Set(1, 2, 3, 4).fold(0, (acc, i) => acc + i) // 10
Atenção: Não assumir nada sobre a ordem em que os elementos são iterados.
Exercício: Re-escreva nossos exemplos anteriores usando fold ao invés de map e filter:
Você vai precisar usar:
s1 e s2: s1.union(s2)if (cond) bloco1 else bloco2unionintersectexcludein, containse.in(S) é equivalente a S.contains(e)subseteqforallexistsSet(1, 2).powerset() // Set(Set(), Set(1), Set(2), Set(1, 2))
Útil quando queremos gerar várias possibilidades para escolher dentre elas.
Um conjunto de conjuntos de elementos to tipo t pode ser convertido em um conjunto de elementos do tipo t com o operador flatten.
Set(Set(1, 2), Set(1, 3)).flatten() // Set(1, 2, 3)
Map é a estrutura de dicionário em Quint. Em TLA+, essa mesma estrutura tem nome de função.
O tipo de um mapa é dado por <chave> -> <valor>. Ou seja, um mapa de inteiros para strings tem tipo int -> str.
Criando Maps:
Map(1 -> "a", 2 -> "b") // Map(1 -> "a", 2 -> "b") Set((1, "a"), (2, "b")).setToMap() // Map(1 -> "a", 2 -> "b") Set(1, 2).mapBy(x => if (x < 2) "a" else "b") // Map(1 -> "a", 2 -> "b")
Para obter todas as chaves:
Map(1 -> "a", 2 -> "b").keys() // Set(1, 2)
E os valores?
val m = Map(1 -> "a", 2 -> "b") m.keys().map(k => m.get(k)) // Set("a", "b")
set atualiza um elemento existente, e put pode criar um novo par chave-valor.
val m = Map(1 -> "a", 2 -> "b") m.get(1) // "a" m.set(1, "c") // Map(1 -> "c", 2 -> "b") m.set(3, "c") // runtime error: error: [QNT507] Called 'set' with a non-existing key m.put(3, "c") // Map(1 -> "a", 2 -> "b", 3 -> "c")
setBy é uma utilidade para quando queremos fazer uma operação sobre um valor existente no mapa.
val m = Map("a" -> 1, "b" -> 2) m.set("a", m.get("a") + 1) // Map("a" -> 2, "b" -> 2) m.setBy("a", x => x + 1) // Map("a" -> 2, "b" -> 2)
Para criar todos os Maps possíveis dado um domínio e um co-domínio, podemos usar o setOfMaps:
Set(1, 2).setOfMaps(Set("a", "b")) // Set(Map(1 -> "a", 2 -> "a"), Map(1 -> "b", 2 -> "a"), // Map(1 -> "a", 2 -> "b"), Map(1 -> "b", 2 -> "b"))
Tuplas são combinações de tipos diferentes em um mesmo valor, onde a ordem dos elementos é o que define o tipo esperado.
O tipo de uma tupla é dado por (t0, ..., tn). Uma tupla com tipo (int, str, bool) permite valores como (1, "a", true).
Existe um único jeito de criar uma tupla:
(1, "a", true)
Itens de tuplas são acessados com ._1, ._2, ._3, …
Não existe ._0, a contagem inicia do 1.
val t = (1, "a", true) t._1 // 1 t._3 // true
Para criar um conjunto com todas as tuplas possíveis com elementos em dados conjuntos, usamos o tuples:
tuples(Set(1, 2), Set("a", "b")) // Set((1, "a"), (2, "a"), (1, "b"), (2, "b")) tuples(Set(1), Set("a", "b"), Set(false)) // Set((1, "a", false), (1, "b", false))
Records são combinações de tipos diferentes em um mesmo valor, onde os elementos são nomeados.
O tipo de um record é dado por { field0: t0, ..., fieldn: tn }. Um record com tipo { nome: str, idade: int } permite valores como { nome: "Gabriela", idade: 26 }.
val r = { nome: "Gabriela", idade: 26 } r.nome // "Gabriela" r.with("idade", 27) // { nome: "Gabriela", idade: 27 } { ...r, idade: 27 } // { nome: "Gabriela", idade: 27 } r // { nome: "Gabriela", idade: 26 }
Listas são como conjuntos, porém com uma ordem definida e, possivelmente, com elementos repetidos. Em TLA+, essa mesma estrutura tem nome de sequência.
O tipo de uma lista é dado por List[<elemento>]. Ou seja, uma lista de inteiros tem tipo List[int].
Criando listas:
[1, 2, 3] // [1, 2, 3] List(1, 2, 3) // [1, 2, 3] range(1, 4) // [1, 2, 3]
val l = [1, 2, 3] l[1] // 2 l.head() // 1 l.tail() // [2, 3]
val l = [1, 2, 3] l.replaceAt(0, 5) // [5, 2, 3] l.concat([4, 5]) // [1, 2, 3, 4, 5] l.append(4) // [1, 2, 3, 4] l // [1, 2, 3]
slice retorna uma nova lista com um intervalo de elementos da lista original.
[1, 2, 3].slice(0, 1) // [1]
select é semelhante ao filter (de conjuntos).
[1, 2, 3, 4, 5].select(x => x > 3) // [4, 5]
Diferente do fold pra conjuntos, a operação de fold sobre listas respeita uma ordem específica. foldl (fold left) vai iterar da esquerda pra direita, enquanto foldr (fold right) vai iterar da direita pra esquerda.
Atenção também para a ordem dos argumentos do operador dado como último argumento.
[1, 2, 3].foldl([], (acc, i) => acc.append(i)) // [1, 2, 3] [1, 2, 3].foldr([], (i, acc) => acc.append(i)) // [3, 2, 1]
O operador map não funciona pra listas. Conseguimos reproduzir essa funcionalidade usando o operador indices, que returna o índices de uma lista (isso é, \(0\) até \(length(l) - 1\)).
val l = [1, 2, 3] def f(x) = x + 1 l.indices().map(i => f(l[i])) // Set(2, 3, 4)
Perceba que o resultado aqui é um conjunto. Para que o resultado seja uma lista, temos que usar foldl ou foldr.
Nomes de tipos devem sempre iniciar com letra maiúscula.
type Idade = int val a: Idade = 1
type Periodo = Manha | Tarde | Noite type EstadoLogin = Logado(str) | Deslogado type Opcional[a] = Algum(a) | Nenhum
records do tipo { nome: str, idade: int }, escreva um operador que recebe esse conjunto e retorna a média de idade.records do tipo { nome: str, idade: int }, escreva um operador que recebe esse conjunto e retorna um mapa de nome pra idade.