Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fixed links #1467

Merged
merged 2 commits into from
Aug 7, 2024
Merged

fixed links #1467

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
52dc253
fixed links
MahtabNorouzi Jul 26, 2024
5672d08
Merge branch 'main' into MahtabNorouzi-patch-2
MahtabNorouzi Aug 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ development tooling.

Here is a small specification for a bank:
``` bluespec

module bank {
/// A state variable to store the balance of each account
var balances: str -> int
Expand Down Expand Up @@ -89,13 +90,15 @@ module bank {
}
```


This design lacks some important checks, and we can use the Quint CLI to find a
violation to the `no_negatives` property, which ideally should hold:

```sh
$ quint run bank.qnt --invariant=no_negatives
```


And the result is a violation where address `"alice"` has balance `-79` in the second state.

``` bluespec
Expand Down Expand Up @@ -147,7 +150,7 @@ Quint is inspired by [TLA+][] (the language) but provides an alternative surface
syntax for specifying systems in TLA (the logic). The most important feature of
our syntax is that it is minimal and regular, making Quint an easy target for
advanced developer tooling and static analysis (see our [design
principles](./doc/design-principles.md) and [previews](./doc/previews.md) of the
principles](./docs/pages/docs/design-principles.md) and [previews](./docs/pages/docs/previews.md) of the
tooling).

The syntax also aims to be familiar to engineers:
Expand Down Expand Up @@ -222,9 +225,10 @@ Cosmos in 2023.

## Documentation


View the [Quint documentation](https://quint-lang.org/docs).

We aspire to having great, comprehensive documentation. At present, we have a
We aspire to have great, comprehensive documentation. At present, we have a
good start, but still far to go. Please try what we have available and share
with us any needs we have not yet been able to meet.

Expand Down
Loading