Untitled1.ipynb

untitled1.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "name": "Untitled1.ipynb",
      "provenance": [],
      "collapsed_sections": [],
      "authorship_tag": "ABX9TyPRwHswBJffxqAgJCRLpyn/",
      "include_colab_link": true
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "view-in-github",
        "colab_type": "text"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/gist/enakai00/c03fbd64a435b1269ce13c8d40d036b7/untitled1.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "bG1YQYGJZWuF",
        "outputId": "8e08886e-c78a-4a48-a73e-f493596ed93c"
      },
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "[10, 4, 8, 1, 6, 3, 3, 2, 6, 7]\n",
            "[4, 10, 8, 1, 6, 3, 3, 2, 6, 7]\n",
            "[4, 8, 10, 1, 6, 3, 3, 2, 6, 7]\n",
            "[1, 4, 8, 10, 6, 3, 3, 2, 6, 7]\n",
            "[1, 4, 6, 8, 10, 3, 3, 2, 6, 7]\n",
            "[1, 3, 4, 6, 8, 10, 3, 2, 6, 7]\n",
            "[1, 3, 3, 4, 6, 8, 10, 2, 6, 7]\n",
            "[1, 2, 3, 3, 4, 6, 8, 10, 6, 7]\n",
            "[1, 2, 3, 3, 4, 6, 6, 8, 10, 7]\n",
            "[1, 2, 3, 3, 4, 6, 6, 7, 8, 10]\n"
          ]
        }
      ],
      "source": [
        "import random\n",
        "\n",
        "a = [random.randint(0, 10) for _ in range(10)]\n",
        "n = len(a)\n",
        "\n",
        "for i in range(0, n):\n",
        "  for j in range(0, n):\n",
        "    if a[i] < a[j]:\n",
        "      a[i], a[j] = a[j], a[i]\n",
        "  assert a[:i] == sorted(a[:i]) # Loop invariant\n",
        "  print(a)\n"
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "上記のコードは下記のコードと等価"
      ],
      "metadata": {
        "id": "VfhuFlp3tLyn"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "import random\n",
        "\n",
        "a = [random.randint(0, 10) for _ in range(10)]\n",
        "n = len(a)\n",
        "print(a)\n",
        "for i in range(0, n):\n",
        "\n",
        "  # ここに来た時点で a[:i] はソート済み \n",
        "  assert a[:i] == sorted(a[:i]) # Loop invariant\n",
        "\n",
        "  # 以下のループは a[i] をソートを保って a[:i-1] に挿入する\n",
        "  for j in range(0, i):\n",
        "    if a[i] < a[j]:\n",
        "      a[i], a[j] = a[j], a[i]\n",
        "\n",
        "  # ここに来た時点で a[:i+1] はソート済み \n",
        "  assert a[:i+1] == sorted(a[:i+1]) # Loop invariant\n",
        "\n",
        "  # 以下のループは a[i] を a[i+1:] の最大値に置き換える\n",
        "  #（無駄な処理だけど、「a[:i+1] はソート済み」という条件は破壊しないので無害）\n",
        "  for j in range(i, n):\n",
        "    if a[i] < a[j]:\n",
        "      a[i], a[j] = a[j], a[i]\n",
        "\n",
        "  # ここに来た時点で a[:i+1] はソート済み \n",
        "  assert a[:i+1] == sorted(a[:i+1]) # Loop invariant\n",
        "\n",
        "  print(i, a)\n"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "oG8L95Evs90V",
        "outputId": "a0230840-b7ab-41b2-9505-5b6fcc2d3887"
      },
      "execution_count": 18,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "[9, 10, 4, 10, 5, 3, 7, 8, 2, 8]\n",
            "0 [10, 9, 4, 10, 5, 3, 7, 8, 2, 8]\n",
            "1 [9, 10, 4, 10, 5, 3, 7, 8, 2, 8]\n",
            "2 [4, 9, 10, 10, 5, 3, 7, 8, 2, 8]\n",
            "3 [4, 9, 10, 10, 5, 3, 7, 8, 2, 8]\n",
            "4 [4, 5, 9, 10, 10, 3, 7, 8, 2, 8]\n",
            "5 [3, 4, 5, 9, 10, 10, 7, 8, 2, 8]\n",
            "6 [3, 4, 5, 7, 9, 10, 10, 8, 2, 8]\n",
            "7 [3, 4, 5, 7, 8, 9, 10, 10, 2, 8]\n",
            "8 [2, 3, 4, 5, 7, 8, 9, 10, 10, 8]\n",
            "9 [2, 3, 4, 5, 7, 8, 8, 9, 10, 10]\n"
          ]
        }
      ]
    }
  ]
}