Logika
Download
Documentation
Course Notes
Sireum Logika Documentation
Sireum Logika Documentation
Sireum Logika Documentation
¶
1. Getting Started
1.1. Using Sireum v3 Binary Distribution
1.1.1. Installation
1.1.2. Running Logika using Sireum CLI
1.1.3. Updating Logika
1.2. Using Sireum v3 Source Distribution
1.2.1. Prerequisites
1.2.1.1. macOS
1.2.1.2. Linux
1.2.1.3. Windows
1.2.2. Installing and Running Logika
1.2.3. Updating Logika
1.3. Verifying Examples using Sireum CLI
1.4. Logika Command-Line Configuration
1.4.1. Auto Mode
1.4.2. Formula
1.4.3. Last Mode
1.4.4. Timeout
1.4.5. Satisfiability Checking Mode
1.4.6. Symbolic Execution Mode
1.4.7. Integer Bit-Width
1.4.8. Symbol Conversion
1.4.9. C Translation
1.4.10. Server Mode
2. IntelliJ-based Logika Integrated Verification Environment (LIVE)
2.1. LIVE Features
2.2. LIVE Install
2.2.1. Prerequisites
2.2.2. Installing Sireum v3 Plugin
2.3. Optional Settings
2.3.1. Configuring Scala and Scala Worksheet Settings
2.3.2. Using A Fixed-Width Font
2.4. LIVE Update
2.4.1. Using Sireum v3 Binary Distribution
2.4.2. Using Sireum v3 Source Distribution
2.5. LIVE Examples
2.6. LIVE Actions
2.7. LIVE Shortcuts
2.8. Sireum LIVE Configuration
2.8.1. Sireum Settings
2.8.1.1. Sireum v3 Directory
2.8.1.2. VM Arguments
2.8.1.3. Environment Variables
2.8.2. LIVE Settings
2.8.2.1. Syntax Highlighting
2.8.2.2. File Extensions
2.8.2.3. Effects
2.8.2.4. Background Analysis and Idle Time
2.8.2.5. Hint Generation
2.8.2.6. Summoning Incriptions
2.8.2.7. Cone of Influence for Summonings
3. The Logika Formal Input Language
3.1. Basic Language Elements
3.1.1. Identifiers
3.1.2. Operators and Literals
3.1.3. Keywords
3.1.3.1. Scala Keywords
3.1.3.2. Types
3.1.3.3. Built-in Functions
3.1.3.4. Contracts
3.1.3.5. Justifications
3.1.4. Comments
3.1.5. Newlines and Whitespaces
3.1.6. Grammatical Rules
3.2. Propositional Logic
3.2.1. Sequent
3.2.2. Proof
3.2.3. Proof Scoping Rules
3.2.4. Proof Schematic Pattern
3.2.5. Claim Expression
3.2.5.1. Newlines in Expression
3.2.5.2. Expression Equivalence (
≡
)
3.2.6. Justification and Inference Rules
3.2.6.1. Premise
3.2.6.2. And-Introduction (∧i)
3.2.6.3. And-Eliminations (∧e1, ∧e2)
3.2.6.4. Or-Introductions (∨i1, ∨i2)
3.2.6.5. Or-Elimination (∨e)
3.2.6.6. Implication-Introduction (→i)
3.2.6.7. Implication-Elimination (→e)
3.2.6.8. Negation-Introduction (¬i)
3.2.6.9. Negation-Elimination (¬e)
3.2.6.10. ⊥-Elimination (⊥e)
3.2.6.11. Proof-by-Contradiction (pbc)
3.2.7. Propositional Logic Input Language Grammar
3.3. Predicate Logic
3.3.1. Extended Sub-Proof Assumption Step
3.3.2. Extended Claim Expression
3.3.2.1. First-Order Uninterpreted Predicate and Function Applications
3.3.2.2. Universally and Existensially Quantified Claims
3.3.3. Well-Formed-Ness
3.3.4. Abstract Notations and Substitution
3.3.5. Quantified Claim Justification and Inference Rules
3.3.5.1. Forall-Introduction (∀i)
3.3.5.2. Forall-Elimination (∀e)
3.3.5.3. Exists-Introduction (∃i)
3.3.5.4. Exists-Elimination (∃e)
3.3.6. Predicate Logic Input Language Grammar
3.4. Programming Logic
3.4.1. Program
3.4.2. Statement
3.4.2.1. Variable Declaration and Assignment
3.4.2.2. Assertion and Assumption
3.4.2.3. If-Else Conditional
3.4.2.4. While-Loop
3.4.2.5. Sequence Element Assignment
3.4.2.6. Print
3.4.2.7. Proof
3.4.2.8. Sequent
3.4.3. Expression
3.4.3.1. Runtime Checks
3.4.4. Invariant
3.4.5. Method Declaration
3.4.6. Method Invocation
3.4.7. Fact
3.4.8. Extended Assume Step
3.4.9. Extended Claim Expression
3.4.10. Extended Justification and Inference Rules
3.4.10.1. Or-Elimination (∨e)
3.4.10.2. Quantified Claim Inference Rules (∀i, ∀e, ∃i, ∃e)
3.4.10.3. Fact (fact)
3.4.10.4. Invariant (invariant)
3.4.10.5. Substitutions (subst1 and subst2)
3.4.11. Summonings
3.4.11.1. Algebra (algebra)
3.4.11.2. Auto (auto)
3.4.12. Well-formed-ness
3.4.13. Programming Logic Input Language Grammar