Program WHILE to jedno z narzędzi teorii obliczalności służące do ustanowienia, czy dana funkcja jest obliczalna.
Cechy Klasa funkcji obliczalnych za pomocą WHILE odpowiada klasie funkcji obliczalnych za pomocą maszyny Turinga lub programów GOTO. Programy WHILE bazują syntaktycznie i semantycznie, z wyjątkiem pętli WHILE, na programach LOOP.
Formalna definicja Składnia Programy WHILE składają się z symboli: WHILE, DO, END, +, -, :=, ;, oraz dowolnej liczby zmiennych i stałych, przy czym stałe są elementami zbioru liczb naturalnych.
Program P jest syntaktycznie zdefiniowany w notacji BNF jako:
gdzie: jest stałą, są zmiennymi to programy WHILE
Semantyka Wszystkie użyte w danym programie zmienne zostają zainicjalizowane przed wykonaniem programu. Zmienne nie zainicjalizowane bezpośrednio otrzymują domyślną wartość 0.
Wyrażenie postaci
xi := xj + c
oznacza przyznanie zmiennej wartości otrzymanej poprzez dodanie zmiennej i stałej Specjalnym przypadkiem jest tutaj sytuacja, gdzie wartość stałej jest równa zeru.