1. Логика Хоара:
   Логика Хоара — это широко используемый метод аксиоматической семантики, который использует пред- и постусловия для определения поведения операторов. Это позволяет нам рассуждать о корректности программ, доказывая, что предварительные условия выполняются до выполнения оператора, а постусловия выполняются после него. Вот простой пример кода на Python:

def divide(x, y):
    # Pre-condition: y is not 0
    assert y != 0
    # Post-condition: x divided by y is returned
    return x / y

2. Логика Флойда-Хора:
   Логика Флойда-Хора — это расширение логики Хоара, которое вводит инварианты цикла, то есть условия, которые выполняются до и после каждой итерации цикла. Это позволяет рассуждать о корректности циклов. Рассмотрим следующий фрагмент кода:

def factorial(n):
    # Pre-condition: n is a non-negative integer
    assert n >= 0
    result = 1
    i = 1
    # Loop invariant: result contains the factorial of i - 1
    while i <= n:
        result *= i
        i += 1
    # Post-condition: result contains the factorial of n
    return result

3. Динамическая логика:
   Динамическая логика — это еще один метод аксиоматической семантики, который расширяет логику Хоара путем включения операторов темпоральной логики для анализа динамического поведения программ. Это позволяет нам выражать свойства, которые сохраняются во времени или в нескольких состояниях программы. Вот упрощенный пример использования псевдокода:

{ x = 0 }
while x < 10:
    { x < 10 }
    x = x + 1
    { x > 0 }
{ x = 10 }

4. Логика разделения:
   Логика разделения — это мощный аксиоматический семантический метод, используемый для рассуждения о программах, которые манипулируют динамически выделяемой памятью. Он вводит пространственные операторы, чтобы выразить, как различные части памяти взаимодействуют и изменяются во время выполнения программы. Вот простой фрагмент кода на языке C:

int* allocate(int size) {
    // Pre-condition: size is greater than 0
    assert size > 0;
    int* ptr = malloc(size * sizeof(int));
    // Post-condition: the allocated memory is valid
    assert ptr != NULL;
    return ptr;
}