Skip to content

An experiment in verifying a small programming language

License

Notifications You must be signed in to change notification settings

hydrolarus/chambo

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

4 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

chambo

chambo is a language to explore the implementation of verification primitives.

The verification primitives are

  • requires clauses on functions as preconditions
  • ensures clauses on functions as postconditions
  • assert expression

The language is split in a "term" and an "expression" part. The "expression" part is meant to be trivially executable on a CPU at runtime. The "term" part is meant to express logical predicates, including harder-to-execute concepts like universal and existential quantifiers.

Verification primitives use the "term" language.

For an example, see the example directory.

License

This code is licensed under the EUPL-1.2 license.

About

An experiment in verifying a small programming language

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published