読者です 読者をやめる 読者になる 読者になる

refineの例

Coq

Coqを勉強していたら、refineタクティクというものに出会った。一緒にSpecif moduleのsigの記述もあったので最初は混乱していたものの、何となく把握してきた。使い方は次のような感じ。 Definition pred (n : nat) : n>0 -> nat. refine (match n with | 0 …

任意の自然数a,b,cについてa*a+b*b=c*cのときにa,b,cすべてが奇数ではないことを証明してみた

Coq

Coqネタ。挑戦してみていろいろ勉強になった。試行錯誤はやっぱり勉強になる。勉強中はバックトラックでもタダでは起きない(キリッ 時間かかり過ぎですが。今回はタイトル通り、「任意の自然数a, b, cについて a*a+b*b=c*c のとき、a, b, cすべてが奇数ではな…

XP一日体験ワークショップに参加してきたったー

さんかしてきたったー・・・で終わったらだめか。 XP一日体験ワークショップに参加してきました。今回はTDD、ペアプログラミング、CIによる受け入れテストがメインでした。一応参加しての感想をば。 ソロドロー&ペアドロー(泣 一人でと、二人で作業をやる…

JenkinsとGitとSpockで独り継続的インテグレーション

明日は大阪で楽しくXPを体験してこようと思ってます、なおきりんです。(XP一日体験ワークショップ! - http://kokucheese.com/event/index/30196/)今回、継続的インテグレーションが参加するイベントの一つにあげられているので、先取りで独り継続的インテ…

Coq to OCamlで便利な標準ライブラリ(型変換)

先日Coqの関数をOCamlのコードとして出力してみました。サンプルとしては (* ret_num.v *) Definition ret_num (n : nat) : nat := n. Extraction "ret_num.ml" ret_num. を coqc ret_num.vして (* ret_num.ml *) type nat = | O | S of nat (** val ret_num…

今後の進路決定があったので書き残しておく

決まったことがあるので、いろいろ書き残しておくことにします。 まずは内定 とある第一志望の企業に内定もらいました。 職種はソフトウェアエンジニアです。身に余る高い評価をいただいたと思っているので、これから一年間いろいろがんばってみようと思って…

逃げないことはそれだけで才能だと思った

唐突で申し訳ないのですが、タイトルのようなことを思ったのでそう書きました。大したことも書いてない記事で、いつものような勉強の事ではないです。

来春プログラミングする人のためのTODO list

来春プログラミングするのは私です。人にお勧めしたいことも含みつつ、書いてみることにします。(自分のために書いているので、やってないことも含みますがご了承ください。) Coq http://coq.inria.fr/ 定理証明支援器として知られるCoqです。 特定の値に対…

Coqの練習(2)

Coq

前回に引き続き、練習してます。今回はちょうど見つけたCoq-99 : Part 1の問題をやってみました。一応、答えを見ずに全部できましたが、所々詰まったりしました。ある意味、人間バックトラックです。 Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B)…

Coqの練習(1)

Coq

突然ですが、皆さんは定理証明支援器ってご存知ですか。 定理証明支援器というのは、命題論理の定理を半自動で証明することを可能にしてくれるツールです。去年の末、「テスト?ちがうちがう。これからの時代は証明だよ!」という話になったので、どうせOCam…

プログラミング言語の難しさとは(いろんな言語に触れてみてほしいと思って考えてみたこと)

最近友人と話していると思うのは、人によって言語やパラダイムに対しての価値観や捉え方がかなり違っていることです。私はどの言語も使いこなせるほどの能力はないですし、ちょっとしたプログラムを書いたことしかないような言語もたくさんあります。 ただ自…

lablglut + Windows でちょっとハマったのでメモ

ハマったと言っても大してハマったわけではないので、あとでlablglutの記事を書いてそちらに統合したいと思ってます。 Windows上でOCaml + lablglutで遊んでみていたのですが、どうもリンクが上手く言ってない模様でした。 > ocamlopt -I +lablGL lablglut.c…

ラムダ計算をちょっと勉強してみたので、忘れないうちに書いておく

なんとなく最近少し理論的な方面もやってみようかなと思い立って、今回はラムダ計算の基礎を勉強してみることにしました。 関数型言語の基盤らしいです。たしかにちょっと雰囲気はあります。参考にしたページとしてはWikipedia ラムダ計算 - http://ja.wikip…

就活は結構性格が出る?

今回はネタ投稿です。ただ単に就活となるとやっぱりみんな性格が出るのかな、と言うお話です。 逆に就職支援とかはこういう意味で性格診断とか先にやった上で個人の性格にあった支援すればいいんじゃないかなーとか思ったり。そんなことはさておき、ちょっと…

pa_monadで遊んでみた

OCamlのモナド拡張、pa_monadで遊んでみました。今回はリスト内の値を長さとする棒を組み合わせて三角形ができる場合に、その周長が最大になるものをpa_monadを使ってListモナドで求めてみました。 open List (* Listモナド *) module ListM = struct let re…

TDDのテスト vs. QAのための単体テスト について考えてみた

最近ソフトウェアテストについての知識を深めようと頑張っている中でTDDのテストとQAのための単体テストの差というものを考えてみたくなりました。もちろんこれらが違うものであることは認識にあったのですが、より正確に認識するために、そして人に聞かれて…

JavaFXに触れてみた Part2

この前の記事でJavaFXの簡単な紹介をしました。 JavaFXに触れてみた今回はその続きでもう少しどのように使うかを書いていこうと思います。 前回はJavaFXのトップレベルのコンテナ(基本的にはウィンドウレベルの情報を保持している)とウィンドウ内の表示領域…

JavaFXに触れてみた

最近GroovyとかClojureとかを触ってた影響で、Javaのライブラリとかフレームワークを使うことが増えてきました。その中で、今回はJavaFX2.0に触れてみたのでちょっとだけ使い方を書いておきます。 まあ、Web上に既にかなりの量の情報が上がっているので、誰…

WACATE2011冬に参加してきました

今回、WACATE2011冬に参加してきました。WACATEは「若手テストエンジニアによる、若手テストエンジニアのための、若手エンジニア向けワークショップ」ということで、たくさんのテストエンジニアの方にお会いすることができました。ちなみに私はテストエンジ…

私が考えるTDD 〜TDDは天才にしかできないのか〜

TDD Advent Calendarに参加していないのに書くのも微妙なのですが、今回はTDDについてです。TDD Advent Calendarの記事はかなりハイスペックな内容になっています。今回の私の記事はそれらには到底及ばないと思いますが、私の考えるTDDを書いて行こうと思い…

Clojureでテストを書く (with TDD)

Clojureでテストを書く、というのはclojure.testというものを用いることで簡単に達成できます。今回はTDDを進めていく体で、テストの書き方を紹介していこうと思います。 お題は簡単に行うためにFizzBuzz*1です。FizzBuzzについてはWeb上に多く紹介があると…

JSONファイルを処理するコードをClojureで書いてみよう

タイトルで「JSONファイルを処理するコードをClojureで書いてみよう」などと言っていますが、ほとんどすることはありません。基本的にはclojure.contrib.jsonを使って、JSON形式の文字列(およびJSONファイル)とClojureのマップの相互変換してもらえばいいだ…

Clojureでコマンドラインオプションを処理してみよう

Clojureでコマンドラインのオプションを処理するための便利なマクロがあります。それがclojure.contrib.command-lineです。早速ですが使い方を見てみます。 (ns sample.core (:use [clojure.contrib.command-line :only (with-command-line)]) (:use [clojur…

Clojureで簡易DSLを書いてみよう

今回は本当に簡単なDSL(もどきですが…)を書くということを行ってみます。 (defdsl :foo "foo" :bar "bar" :num 3 :data ["a" "b" "c"]) のようにファイルに書かれたDSLを読みこんで処理することを想定します。 (もちろんこれはClojureのコードになっています…

leiningenでClojureをビルドしよう

独りAdvent Calendar 第2弾として、Clojureについて書いていこうと思います。Clojureは私自身最近始めたばかりの言語で、1ヶ月ほど合間を見ながら少しずつやってきた言語です。 そのため、あまりよいコードになっていなかったり、Clojureっぽくない書き方に…

私が使うGitコマンドまとめ のまとめ

Git

12/1〜12/8までのGitの記事のリンクをまとめました。 さすがに、こういうページがないと自分でもつらい・・・私の使うGitコマンドまとめ 基本コマンド編私の使うGitコマンドまとめ 見る編私の使うGitコマンドまとめ ブランチ&タグ編私の使うGitコマンドまと…

私の使うGitコマンドまとめ 逆引き編

Git

「私の使うGitコマンドまとめ」の記事を、逆引きとして使えるようにしてみました。 私がよく行っていることを「私の使うGitコマンドまとめ」の記事では書いていないオプションの組み合わせなども書きました。目次 HEAD、インデックス、ワーキングツリーを理…

Gitの基礎知識 コマンド以外に知っておくべきこと

Git

Gitにはコマンド操作をする際に知っておくべきことが数多くあります。そのうちでも最低限知っておくべきことを書いてみることにしました。 Gitを使いこなすにはもっともっと必要な知識は数多くあります。 もっと知りたい方はいろいろと調べてみることをお勧…

私の使うGitコマンドまとめ その他編

Git

それほど頻繁には使いませんが、ちょっとしたことで使うコマンドについてまとめます。 git update-index (リポジトリですでに管理しているファイルを無視する) git gc (リポジトリを最適化する) git fsck (リポジトリの正当性を調べる) git update-index (リ…

私の使うGitコマンドまとめ リモート編

Git

今回はリモートリポジトリを操作するコマンドをまとめます。リモートリポジトリの操作は同じような操作をする際にもローカルリポジトリとは異なっていたり、お作法としてしてはいけないこともあります。 そういう点は気をつけて使ってみましょう。 git clone…

私の使うGitコマンドまとめ 歴史操作編

Git

Gitでバージョン管理をしていく際に、どうしても間違ったコミットやバグを含む内容の修正、ブランチの統合などを行う必要があります。 そういうときに使えるコマンドを今回は書いていきます。ブランチのマージなどはブランチのまとめの方に書くべきかもしれ…

私の使うGitコマンドまとめ ブランチ&タグ編

Git

バージョン管理システムではよく行われるブランチを切るということ。Gitでは分散バージョン管理であることを生かして、ローカルとリモート(中央リポジトリ)で違うブランチの状態を作ることが可能です。 つまりローカルで好きにブランチを切っておくことも…

私の使うGitコマンドまとめ 見る編

Git

前回はGitを使う上で絶対に必要なコマンド(+オプション)について書いてみました。実際には他にも必要なコマンドはたくさんありますが、今回はそのうちでも「見る」ということに焦点を当てたコマンドをまとめてみようと思います。 git status (現在の状態を…

私の使うGitコマンドまとめ 基本コマンド編

Git

独りAdvent Calendarへの挑戦の一発目として、私がよく使うGitのコマンドをまとめていくことにします。 あまり使いこんではいないので役に立つかわかりませんが書いていきます。 git init (リポジトリの作成) git add (管理するファイルの指定) git rm (ファ…

独りAdvent Calendar はじめます

独りAdvent Calendarをやろうと思います。多分、いろいろ忙しかったりネットが使えない日とかがあるので、先に投稿したり、遅れて投稿したりすることにはなると思いますが、25日まで頑張ろうと思います。以下、Advent Calendar記事のリンクです。12/1 私の使…

Clojureの"->"(arrow)マクロ

いろいろClojureを調べていたところ出くわした"->"というマクロが気になったのでリファレンスを見てなんとなく理解した気がするので書いておきます。 アロー(->)なマクロさん 現代的にしようという意図はありつつも、Lisp道をひた走るClojureさん。 連鎖的な…

Boost Explorers Study #1 を開催してみました

開催してみましたとはいえ、GithubのWikiに基本的にはすべて書いているのでブログで書くことはあまりないです。私自身の感想としては、Gitに手間取った印象です。 たぶん、Gitに3時間ほど費やしました。まだまだGitに慣れているとは言えませんし、最近触って…

Cooking for Geeks を読んで料理に挑戦! (2)

今回はid:pocketberserkerさんと一緒に料理しました。作ったのはポークビーンズ。豚肉を挽き肉にするかこま肉にするか悩んだのですが、pocketberserkerさんの希望によりこま肉にしました。 作って食べてみると、こま肉にトマトの味が絡んでなかなかおいしか…

boost::optional と boost::logic::tribool の違い

C++

boost::optionalの説明でも書かれていますが、一応メモ。 boost::triboolは3値論理と言われるものを表現するための型です。 一般の論理値、true, falseに加えて、indeterminate(不定)というものが加わっています。 これはboost::optionalに非常によく似てい…

プログラマ35歳定年説について就職前の学生が考えてみた

最近、よくプログラマ35歳定年説についてのブログの記事がTwitterで流れてきます。実際はもともと有名な話で、おそらくたまたまTwitterでフォローしている人数が増えたから多くなったように感じているだけだと思います。でも、私もそちらの業界を目指す学生…

Clojureの引数や関数の戻り値にキャストの情報を与える

Clojureは動的型付け言語です。つまり、変数や関数の戻り値、引数の型宣言はありません。 (defn hoge [s] (.toUpperCase s)) でも、結局のところ、引数に渡すオブジェクトや関数の戻り値で使っているのはJavaのクラスのオブジェクトだったりするわけです。さ…

Cooking for Geeks を読んで料理に挑戦! (1)

Cooking for Geeks ―料理の科学と実践レシピ (Make: Japan Books)作者: Jeff Potter,水原文出版社/メーカー: オライリージャパン発売日: 2011/09/22メディア: 大型本購入: 40人 クリック: 2,561回この商品を含むブログ (35件) を見るCooking for Geeks読んだ…

Cooking for Geeks を読んでみる(2)

Cooking for Geeks ―料理の科学と実践レシピ (Make: Japan Books)作者: Jeff Potter,水原文出版社/メーカー: オライリージャパン発売日: 2011/09/22メディア: 大型本購入: 40人 クリック: 2,561回この商品を含むブログ (35件) を見る最近、この本にはまって…

Cooking for Geeks を読んでみる(1)

Cooking for Geeks ―料理の科学と実践レシピ (Make: Japan Books)作者: Jeff Potter,水原文出版社/メーカー: オライリージャパン発売日: 2011/09/22メディア: 大型本購入: 40人 クリック: 2,561回この商品を含むブログ (35件) を見る今日買いました。面白い…

ClojureでFizzBuzzを書いてみた with テストコード

ClojureでFizzBuzzをテスト付きで書いてみました。Clojure自体がなかなかつかめなくて、さすがにTDDできるほど余裕がなかったです… ; 名前空間の定義と ; test用の関数を使うために:useでclojure.testをロード (ns fizzbuzz (:use clojure.test)) ; 実際のFi…

佐賀Groovy勉強会を開催しました

9/18(日)に佐賀Groovy勉強会を開催しました。元々Groovyの勉強会が開催されている地域がかなり限定されていることもあって妙に注目してもらっていたようです。私自身はそこまで注目されるとは思っていなかったのですが…ただUstreamを流す予定が、どうしても…

佐賀Groovy勉強会 演習のお題

佐賀Groovy勉強会で今回行う予定のお題です。 1. 小町算 小町算を行い、その結果を表示するプログラムを作成し、それをGParsを用いて並列計算することで高速化を図ってください。 まずはwithPoolを使ってみることをお勧めします。 小町算は1×2×3×4+5+6+7×…

佐賀Groovy勉強会を開催します

よく考えてみると、この話をブログに書いてなかったですね…9/18(日)に佐賀でGroovyの勉強会を開催します。 募集ページは http://partake.in/events/1b7c7076-7a05-48e8-bd0e-c436b8c2c8c7ちなみにUstreamの生放送もする予定です。 初の勉強会開催ですし、発…

neocomplcacheの設定が上手くいかない…(解決しました)

neocomplcacheの補完機能がいいらしいという噂を聞きつけてやってみようとしたものの…"std::"と打った時は補完されるのですが、"boost::"では補完が効かない。 clangを直接たたいた時は"boost::"でも補完が効くので困ってたり。追記:一応動くようにできまし…

GParsのデータ並列のハロワ的コードを書いてみた

GPars大きいですね…データ並列の部分で書くだけでこんな量になるとは。しかも機能が他にもいろいろあって、全然終わらない。これは腰を据えてやっていかないと全容把握は難しいかも。今回はGroovy 1.8.1とGPars 0.12を使いました。 GParsPool import groovyx…