In the current directory, there are three subdirectories - Meeting Scheduler, Popsicle Finance, and Ticket Depot. Each subdirectory contains a system implemented in Solidity. For each of the systems in this directory, do as follows:
- Try to understand the principles of the given system without going into details of implementation - what it is supposed to do and what mechanism it uses. To do that, you can read the comments and documentation of the file, look at its global variables, and go over the functions' signatures (or the interface if it exists).
ℹ️ You can look at the implementation if you'd like to understand better how things work in the system. However, the implementation should comply with the specifications, not the other way around.
- Think about the properties of the system and write them down in free language - English/logic/pseudo code. Don't worry about writing the properties in CVL. For now, we only practice the identification of properties regardless of implementation feasibility/complexity.
📝 Try to think of at least one property of each type for each system.
- [ ] Write the properties down in your favorite word processor and upload it with the name "<system_name>_properties_solution" to the current directory.
- Classify each of your properties as one of the five types we defined in the presentation Categorizing Properties.
- Prioritize your set of properties as demonstrated in the Auction Demonstration.
- If possible, reach out to a fellow participant of the on-boarding and ask them to discuss your properties. Exchange thoughts and ideas.
📝 The Certora Team will review your solution and give you a personal review. In the next lessons you will exercise thinking about properties some more; please wait for your review before proceeding to the next exercise (Lesson 9) in this subject.
💡 Thinking about properties is a process of brainstorming. It is always recommended to have a partner(s) to discuss your ideas with.