Conditionals
Conditionals let runtime code and specifications split facts into explicit cases. In verified code, each branch is a proof path: postconditions, actor invariants, and declared effects must hold no matter which branch runs.
Pattern Matching
Pattern matching with switch expressions lets you inspect variant tags, options, tuples, and literals while making every case visible to the type checker and verifier.
Loops
Loops let you execute code repeatedly. Sector9 supports while, infinite loop with labeled exits, and for-in iteration over contracted iterators. In verified code, loop invariants are the bridge between each iteration and the final postcondition.
Error Handling
Error handling with try/catch/finally provides structured recovery from failures in async contexts. General Sector9 code can throw errors, but verification mode rejects throw; verified code should model recoverable failure with return values or explicit trap contracts instead.