gabriel-fallen

Вступление

Во-первых, это моё мнение, и я его никому не навязываю. Во-вторых, список не обязательно исчерпывающий. В-третьих, он ориентирован на определённую "философию", которая тоже не является исчерпывающей или абсолютно правильной. Поэтому, если Вам эти рекомендации не подходят -- не следуйте им.

Философия такова. Для того чтобы осмысленно программировать на начальном этапе не нужно знать Computer Science, теорию алгоритмов и сложности вычислений или детально разбираться в устройстве и работе компьютера. Достаточно хорошо делать две вещи:

1. алгоритмизировать решение задачи (разбивать его на простые последовательные шаги: сначала это, а потом вот это),
2. знать, понимать смысл и назначение, использовать и подгонять друг к другу стандартные элементы решений (условия, циклы, структуры данных, алгоритмы и прочие "паттерны")

gabriel-fallen

Презентации и справочники

https://docs.google.com/file/d/0B3gcGsPmNL0VT2RjLVZybTNkclE/edit

Задание 1

1. Установить сервер Apache Tomcat (или другой servlet-compatible сервер)

gabriel-fallen

# in ~/.fluxbox/keys
# change KB layout
# Mod4 k e # English
Mod4 45 26 :Exec setxkbmap us
# Mod4 k r # Russian
Mod4 45 27 :Exec setxkbmap ru

gabriel-fallen

Статьи против Программ

На днях заметил, что читать статьи (по computer science) гораздо сложнее, чем читать/писать программы. Кажется парадоксальным, но вполне объяснимо — всё дело в пресловутом управлении сложностью.

Как известно, объём "кэша" у человека сильно ограничен — одновременно можно думать всего о 5-9 вещах. Может быть, некоторые могут думать об 11 вещах одновременно, но едва ли больше. Если учесть, что как правило нужно помнить не только отдельные объекты, но и связи между ними, то получится удержать в сознании всего 3 (+ 3 связи = 6) или 4 (+ 6 связей = 10) сущности.

gabriel-fallen

(declare-sort Type)
(declare-sort Term)
(declare-fun HasType (Term Type) Bool)

(declare-fun string () Type) ; type of strings of a programming language
(declare-fun nat () Type)    ; type of natural numbers of a programming language
(declare-fun list () Type)   ; type of lists should be parametrized by type of elements but we ignore it for simplicity

(declare-fun BoxString (String) Term)

gabriel-fallen

theory GCD
imports Main
begin

fun gcd :: "nat ⇒ nat ⇒ nat" where
"gcd m 0 = m" |
"gcd m n = gcd n (m mod n)"


theorem gcd_dvd_both: "(gcd m n dvd m) ∧ (gcd m n dvd n)"

gabriel-fallen

module SampleTheorems

%default total

reverse' : List a -> List a
reverse' [] = []
reverse' (x :: xs) = reverse' xs ++ [x]

append_nil : xs ++ [] = xs
append_nil {xs = []} = Refl

gabriel-fallen

#lang racket/gui

;;; Files part

(define (image-files-list dir)
  (filter (lambda (p) (let ([ext (bytes->string/utf-8 (path-get-extension p))])
                        (or (string-ci=? ext ".jpg") (string-ci=? ext ".jpeg") (string-ci=? ext ".png"))))
          (directory-list dir #:build? #t)))

(define images-top    (map read-bitmap (image-files-list "top")))

gabriel-fallen

gabriel-fallen

theory Demo
imports Predicate_Compile Extraction
begin

datatype 'a list = Nil
  | Cons (head: 'a) (tail: "'a list")
  for map: lmap

primrec append :: "'a list ⇒ 'a list ⇒ 'a list" where
  "append Nil ys = ys"