A Strong Typed Computational Model for Shell Languages
Authors
Andersen, Christoffer Lind ; Bonderup, Nikolai Aaen
Term
4. term
Education
Publication year
2024
Submitted on
2024-06-13
Pages
81
Abstract
Shell-sprog som Bash og PowerShell bruges bredt til automatisering og scripts, men svage eller manglende typesystemer kan føre til kørselsfejl, vedligeholdelsesproblemer og sikkerhedsrisici. Dette speciale introducerer λ_sh, et nyt funktionelt shell-sprog med et stærkt, statisk typesystem. Typer er regler for, hvilke slags data funktioner og kommandoer må bruge; når de kontrolleres før kørsel, kan fejl opdages tidligt, og koden bliver nemmere at læse og vedligeholde. λ_sh bygger på lambda-kalkylen, en enkel matematisk model for beregning, som ofte bruges til at beskrive programmeringssprog. Specialet præsenterer formel semantik—præcise regler for, hvordan programmer opfører sig—inklusive operationel semantik, der beskriver trinvis udførelse. Sproget giver eksplicitte og forudsigelige muligheder for at arbejde med tekst, herunder strengsammenkædning (at sætte tekststykker sammen) og interpolation (at indsætte værdier i tekst). Det omfatter også en formel model af shell-miljøet, så kommandoer, variabler og filer interagerer på veldefinerede måder. Samlet set beskriver specialet de teoretiske grundlag, designprincipper og sprogets operationelle regler og viser, hvordan λ_sh søger at bevare shellens fleksibilitet og samtidig opnå type-sikkerhed, tidlig fejlfangst og bedre læsbarhed og vedligeholdelse.
Shell languages like Bash and PowerShell are widely used for automation and scripting, but weak or missing type systems can lead to runtime errors, maintenance difficulties, and security risks. This thesis introduces λ_sh, a new functional shell language with a strong, static type system. Types are rules about what kinds of data functions and commands can use; checking them before execution catches errors early and makes code easier to read and maintain. λ_sh is grounded in the lambda calculus, a simple mathematical model of computation often used to define programming languages. The thesis presents formal semantics—precise rules for how programs behave—including operational semantics that describe step-by-step execution. The language provides explicit and predictable features for working with text, including string concatenation (joining text) and interpolation (inserting values into text). It also includes a formal model of the shell environment so that commands, variables, and files interact in well-defined ways. Overall, the thesis details the theoretical foundations, design principles, and operational rules of the language, and shows how λ_sh aims to keep the flexibility users expect from shells while gaining type safety, early error detection, and improved readability and maintainability.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Keywords
Documents