At Runtime Verification, K framework is the backbone of the company. Since the CEO of Runtime Verification, Grigore Rosu, started the K project back in 2003 for teaching purposes, the K framework has evolved, its user base has grown, and there are more use cases than ever in the ecosystem.
If you ended up in this blog post, you are probably somehow familiar with K framework, wanting to learn more, or trying to address some doubts. Well, I'm glad to say that you came to the right place. In this blog post, you will find a guide and link to our tutorial to learn how to prove in K from zero.
Tutorial and Resources
During the last few years, we met many people from the academic ecosystem and developers with different backgrounds interested in learning K or keep learning new things and improving their current skills.
To help as many people as possible and make it easier for everyone to learn about K, we decided to share a video tutorial to follow along and learn, starting from zero, how to prove things in K. This tutorial was initially created for internal use for our team, but we decided that more people could benefit from it if we made it public.
If you plan to follow along with the tutorial, please install or update to the latest K release. We highly recommend following along, stopping and rewatching the video as many times as needed, and coming to discord to ask the team any questions you may have or if you want to keep building on your own and you need further support.
But, before starting with the tutorial, and especially if you are new to K, make sure you check the following resources:
- Repository with solutions: You can refer to this repository if you want to follow along with the video and check the results of the exercises.
- K framework website: It's the holy bible for K. On the website you will find different resources, tutorials, user documentation, built-ins, and a lot more that will be coming soon!
- Github: If you want to dive deeper on K, Github is the place to go. Everything you didn't know you needed will be on the Github page, from different languages semantics to tools and execution engines.
- Discord: If you have any questions following the tutorial or trying your own thing, you can come to discord and ask our developers. We are always happy to help the community and get to know you.
Content
The tutorial videos can be found on our youtube channel and consist of a total of six episodes and six different exercises. Depending on your current knowledge of K, you may want to skip some episodes. If you want to know more about the content of each episode, here is a summary of its content and the video link to each one:
Exercise 1: Calculator & Exercise 2: Calculator with Boolean Expressions
In the first exercise, we will create a calculator and use functional fragments of K to correctly compute integer arithmetic expressions. Examples in tests/01-calc.
In the second exercise, we will finalize the remaining content about functional fragments of K, and we will extend the calculator to deal with boolean expressions too. Examples in tests/02-calc-bool.
Exercise 3: Variables in Expressions, Explicit Substitution
In this 3rd exercise, we will move to the stateful fragment of K, which requires adding a configuration. We can hardcode some variable values in the configuration for now, to allow using them in programs. Examples in tests/03-subst.
Exercise 4: Assignment Operator
In this exercise, we will focus on adding statements, statement sequencing, and an assignment operator. This will allow us to update variables instead of updating the entire definition each time we want to change a variable. Examples in tests/04-assignment.
The second part of this exercise will focus on re-doing the assignment operator, but using the K strict feature instead of substitution for expression evaluation.
Next, we will re-do the assignment operator, but using contextual functions instead of substitution for expression evaluation.
Exercise 5.1: Control Flow
The 5th exercise is split into two different videos. In the first part, we will focus on adding control flow statements to our programming language. We will add an if statement, allowing us to have branches in our programs. Examples in tests/05-control-flow.
Exercise 5.2: Control Flow - Looping Specification
For the second part of the 5th exercise, we will focus on looping specifications. We will add a while loop, allowing us to have loops in our programs. Examples in tests/05-control-flow.
Exercise 6: Procedures
In the final exercise, we will show how to add procedures to our language to be able to bundle up chunks of code and call them in other expressions. Examples in tests/06-procedures.
Join Us
If you enjoyed this tutorial and you want to see more, please come and join us in discord and let us know what you would like us to do next. And, if by any chance you are looking for a career change or you are a student looking for an internship, come and talk to us! We are always looking for exceptional individuals with a passion for formal methods and K to join the team in our office in Urbana, Singapore, or remotely from anywhere in the world.
